Theorems · Theorem · order theory

Set.PairwiseDisjoint.prod_left

∀ {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [inst : CompleteLattice α] {s : Set ι} {t : Set ι'} {f : ι × ι' → α},
  (s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')) →
    (t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')) → (s ×ˢ t).PairwiseDisjoint f

If the suprema of columns are pairwise disjoint and suprema of rows as well, then everything is pairwise disjoint. Not to be confused with Set.PairwiseDisjoint.prod.

Defined in

Mathlib.Data.Set.Pairwise.Lattice

Cited by

1 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CompleteLattice