Mathlib.Order.SupIndep

Finset.SupIndep definition

(s : Finset ι) (f : ι → α) : Prop

Full source

/-- Supremum independence of finite sets. We avoid the "obvious" definition using `s.erase i`
because `erase` would require decidable equality on `ι`. -/
def SupIndep (s : Finset ι) (f : ι → α) : Prop :=
  ∀ ⦃t⦄, t ⊆ s → ∀ ⦃i⦄, i ∈ s → i ∉ t → Disjoint (f i) (t.sup f)

Supremum independence for finite sets

Informal description

A family of elements $ f : \iota \to \alpha $ indexed by a finite set $ s $ is called *supremum independent* if for any subset $ t \subseteq s $ and any index $ i \in s $ not in $ t $, the element $ f(i) $ is disjoint from the supremum of the elements indexed by $ t $. In other words, for all $ t \subseteq s $ and $ i \in s \setminus t $, we have $ f(i) \sqcap (\bigsqcup_{j \in t} f(j)) = \bot $.

Finset.supIndep_iff_disjoint_erase theorem

[DecidableEq ι] : s.SupIndep f ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)

Full source

/-- The RHS looks like the definition of `iSupIndep`. -/
theorem supIndep_iff_disjoint_erase [DecidableEq ι] :
    s.SupIndep f ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f) :=
  ⟨fun hs _ hi => hs (erase_subset _ _) hi (not_mem_erase _ _), fun hs _ ht i hi hit =>
    (hs i hi).mono_right (sup_mono fun _ hj => mem_erase.2 ⟨ne_of_mem_of_not_mem hj hit, ht hj⟩)⟩

Equivalence of Supremum Independence and Disjointness with Supremum of Complement

Informal description

Let $s$ be a finite set of indices and $f : \iota \to \alpha$ be a family of elements in a lattice $\alpha$ with a bottom element $\bot$. Then $f$ is supremum independent on $s$ if and only if for every index $i \in s$, the element $f(i)$ is disjoint from the supremum of the elements indexed by $s \setminus \{i\}$, i.e., $f(i) \sqcap \left(\bigsqcup_{j \in s \setminus \{i\}} f(j)\right) = \bot$.

Finset.instDecidableSupIndepOfDecidableEq instance

[DecidableEq ι] [DecidableEq α] : Decidable (SupIndep s f)

Full source

/-- If both the index type and the lattice have decidable equality,
then the `SupIndep` predicate is decidable.

TODO: speedup the definition and drop the `[DecidableEq ι]` assumption
by iterating over the pairs `(a, t)` such that `s = Finset.cons a t _`
using something like `List.eraseIdx`
or by generating both `f i` and `(s.erase i).sup f` in one loop over `s`.
Yet another possible optimization is to precompute partial suprema of `f`
over the inits and tails of the list representing `s`,
store them in 2 `Array`s,
then compute each `sup` in 1 operation. -/
instance [DecidableEq ι] [DecidableEq α] : Decidable (SupIndep s f) :=
  have : ∀ i, Decidable (Disjoint (f i) ((s.erase i).sup f)) := fun _ ↦
    decidable_of_iff _ disjoint_iff.symm
  decidable_of_iff _ supIndep_iff_disjoint_erase.symm

Decidability of Supremum Independence for Finite Sets

Informal description

For any finite set $s$ and function $f : \iota \to \alpha$ where $\alpha$ is a lattice with a bottom element $\bot$, the property of $f$ being supremum independent on $s$ is decidable when both the index type $\iota$ and the lattice $\alpha$ have decidable equality.

Finset.SupIndep.subset theorem

(ht : t.SupIndep f) (h : s ⊆ t) : s.SupIndep f

Full source

theorem SupIndep.subset (ht : t.SupIndep f) (h : s ⊆ t) : s.SupIndep f := fun _ hu _ hi =>
  ht (hu.trans h) (h hi)

Supremum Independence is Preserved under Subset Inclusion

Informal description

Let $s$ and $t$ be finite sets of indices, and let $f : \iota \to \alpha$ be a family of elements in a lattice $\alpha$ with a bottom element $\bot$. If $f$ is supremum independent on $t$ and $s \subseteq t$, then $f$ is also supremum independent on $s$.

Finset.supIndep_empty theorem

(f : ι → α) : (∅ : Finset ι).SupIndep f

Full source

@[simp]
theorem supIndep_empty (f : ι → α) : (∅ : Finset ι).SupIndep f := fun _ _ a ha =>
  (not_mem_empty a ha).elim

Empty Set is Supremum Independent

Informal description

For any function $f$ from an index set $\iota$ to a lattice $\alpha$ with a bottom element, the empty set is supremum independent with respect to $f$. That is, the empty set satisfies the condition of supremum independence trivially.

Finset.supIndep_singleton theorem

(i : ι) (f : ι → α) : ({ i } : Finset ι).SupIndep f

Full source

@[simp]
theorem supIndep_singleton (i : ι) (f : ι → α) : ({i} : Finset ι).SupIndep f :=
  fun s hs j hji hj => by
    rw [eq_empty_of_ssubset_singleton ⟨hs, fun h => hj (h hji)⟩, sup_empty]
    exact disjoint_bot_right

Singleton Sets are Supremum Independent

Informal description

For any index $i$ and any function $f : \iota \to \alpha$ in a lattice with a bottom element, the singleton set $\{i\}$ is supremum independent with respect to $f$. That is, the element $f(i)$ is trivially disjoint from the supremum of the empty set (which is $\bot$).

Finset.SupIndep.pairwiseDisjoint theorem

(hs : s.SupIndep f) : (s : Set ι).PairwiseDisjoint f

Full source

theorem SupIndep.pairwiseDisjoint (hs : s.SupIndep f) : (s : Set ι).PairwiseDisjoint f :=
  fun _ ha _ hb hab =>
    sup_singleton.subst <| hs (singleton_subset_iff.2 hb) ha <| not_mem_singleton.2 hab

Supremum independence implies pairwise disjointness for finite sets

Informal description

Let $s$ be a finite set and $f : \iota \to \alpha$ a family of elements in a lattice $\alpha$ with a bottom element $\bot$. If $f$ is supremum independent on $s$, then the family $f$ is pairwise disjoint on $s$, i.e., for any two distinct elements $i, j \in s$, the elements $f(i)$ and $f(j)$ are disjoint.

Finset.SupIndep.le_sup_iff theorem

(hs : s.SupIndep f) (hts : t ⊆ s) (hi : i ∈ s) (hf : ∀ i, f i ≠ ⊥) : f i ≤ t.sup f ↔ i ∈ t

Full source

theorem SupIndep.le_sup_iff (hs : s.SupIndep f) (hts : t ⊆ s) (hi : i ∈ s) (hf : ∀ i, f i ≠ ⊥) :
    f i ≤ t.sup f ↔ i ∈ t := by
  refine ⟨fun h => ?_, le_sup⟩
  by_contra hit
  exact hf i (disjoint_self.1 <| (hs hts hi hit).mono_right h)

Characterization of Supremum Independence via Supremum Comparison

Informal description

Let $s$ be a finite set and $f : \iota \to \alpha$ a supremum-independent family of elements in a lattice $\alpha$ with a bottom element $\bot$. For any subset $t \subseteq s$ and any index $i \in s$, if all elements $f(i)$ are non-bottom, then $f(i) \leq \bigsqcup_{j \in t} f(j)$ if and only if $i \in t$.

Finset.SupIndep.antitone_fun theorem

{g : ι → α} (hle : ∀ x ∈ s, f x ≤ g x) (h : s.SupIndep g) : s.SupIndep f

Full source

theorem SupIndep.antitone_fun {g : ι → α} (hle : ∀ x ∈ s, f x ≤ g x) (h : s.SupIndep g) :
    s.SupIndep f := fun _t hts i his hit ↦
  (h hts his hit).mono (hle i his) <| Finset.sup_mono_fun fun x hx ↦ hle x <| hts hx

Monotonicity of Supremum Independence: $f \leq g$ Preserves SupIndep

Informal description

Let $s$ be a finite set and $f, g : \iota \to \alpha$ be two families of elements in a lattice $\alpha$ with a bottom element $\bot$. If $f(x) \leq g(x)$ for all $x \in s$ and $g$ is supremum independent on $s$, then $f$ is also supremum independent on $s$.

Finset.SupIndep.image theorem

[DecidableEq ι] {s : Finset ι'} {g : ι' → ι} (hs : s.SupIndep (f ∘ g)) : (s.image g).SupIndep f

Full source

protected theorem SupIndep.image [DecidableEq ι] {s : Finset ι'} {g : ι' → ι}
    (hs : s.SupIndep (f ∘ g)) : (s.image g).SupIndep f := by
  intro t ht i hi hit
  rcases subset_image_iff.mp ht with ⟨t, hts, rfl⟩
  rcases mem_image.mp hi with ⟨i, his, rfl⟩
  rw [sup_image]
  exact hs hts his (hit <| mem_image_of_mem _ ·)

Supremum Independence Preserved Under Image of Index Set

Informal description

Let $ι$ and $ι'$ be types with decidable equality on $ι$, and let $s$ be a finite set in $ι'$. Given a function $g : ι' → ι$ and a supremum-independent family $f ∘ g$ on $s$, then the family $f$ is supremum-independent on the image of $s$ under $g$.

Finset.supIndep_map theorem

{s : Finset ι'} {g : ι' ↪ ι} : (s.map g).SupIndep f ↔ s.SupIndep (f ∘ g)

Full source

theorem supIndep_map {s : Finset ι'} {g : ι' ↪ ι} : (s.map g).SupIndep f ↔ s.SupIndep (f ∘ g) := by
  refine ⟨fun hs t ht i hi hit => ?_, fun hs => ?_⟩
  · rw [← sup_map]
    exact hs (map_subset_map.2 ht) ((mem_map' _).2 hi) (by rwa [mem_map'])
  · classical
    rw [map_eq_image]
    exact hs.image

Supremum Independence Preserved Under Injective Image of Index Set

Informal description

Let $s$ be a finite set in a type $\iota'$, and let $g : \iota' \hookrightarrow \iota$ be an injective function embedding. A family of elements $f : \iota \to \alpha$ is supremum independent on the image of $s$ under $g$ if and only if the composition $f \circ g$ is supremum independent on $s$.

Finset.supIndep_pair theorem

[DecidableEq ι] {i j : ι} (hij : i ≠ j) : ({ i, j } : Finset ι).SupIndep f ↔ Disjoint (f i) (f j)

Full source

@[simp]
theorem supIndep_pair [DecidableEq ι] {i j : ι} (hij : i ≠ j) :
    ({i, j} : Finset ι).SupIndep f ↔ Disjoint (f i) (f j) := by
  suffices Disjoint (f i) (f j) → Disjoint (f j) ((Finset.erase {i, j} j).sup f) by
    simpa [supIndep_iff_disjoint_erase, hij]
  rw [pair_comm]
  simp [hij.symm, disjoint_comm]

Supremum Independence of a Pair is Equivalent to Disjointness

Informal description

For any two distinct indices $i$ and $j$ in a type $\iota$ with decidable equality, the family of elements $f : \iota \to \alpha$ is supremum independent on the finite set $\{i, j\}$ if and only if the elements $f(i)$ and $f(j)$ are disjoint in the lattice $\alpha$ with a bottom element.

Finset.supIndep_univ_bool theorem

(f : Bool → α) : (Finset.univ : Finset Bool).SupIndep f ↔ Disjoint (f false) (f true)

Full source

theorem supIndep_univ_bool (f : Bool → α) :
    (Finset.univ : Finset Bool).SupIndep f ↔ Disjoint (f false) (f true) :=
  haveI : truetrue ≠ false := by simp only [Ne, not_false_iff, reduceCtorEq]
  (supIndep_pair this).trans disjoint_comm

Supremum Independence of Boolean Family is Equivalent to Disjointness of False and True Cases

Informal description

For any function $f : \text{Bool} \to \alpha$ mapping boolean values to elements of a lattice $\alpha$ with a bottom element, the family $f$ is supremum independent on the finite set of all boolean values if and only if the elements $f(\text{false})$ and $f(\text{true})$ are disjoint in $\alpha$.

Finset.supIndep_univ_fin_two theorem

(f : Fin 2 → α) : (Finset.univ : Finset (Fin 2)).SupIndep f ↔ Disjoint (f 0) (f 1)

Full source

@[simp]
theorem supIndep_univ_fin_two (f : Fin 2 → α) :
    (Finset.univ : Finset (Fin 2)).SupIndep f ↔ Disjoint (f 0) (f 1) :=
  have : (0 : Fin 2) ≠ 1 := by simp
  supIndep_pair this

Supremum Independence on $\mathrm{Fin}\ 2$ is Equivalent to Disjointness of $f(0)$ and $f(1)$

Informal description

For any function $f$ from the finite type $\mathrm{Fin}\ 2$ to a lattice $\alpha$ with a bottom element, the family $f$ is supremum independent on the universal finite set $\mathrm{Finset.univ}$ of $\mathrm{Fin}\ 2$ if and only if the elements $f(0)$ and $f(1)$ are disjoint in $\alpha$.

Finset.supIndep_attach theorem

: (s.attach.SupIndep fun a => f a) ↔ s.SupIndep f

Full source

@[simp]
theorem supIndep_attach : (s.attach.SupIndep fun a => f a) ↔ s.SupIndep f := by
  simpa [Finset.attach_map_val] using (supIndep_map (s := s.attach) (g := .subtype _)).symm

Supremum Independence of Attached Set is Equivalent to Original Set

Informal description

Let $s$ be a finite set and $f : \iota \to \alpha$ a family of elements in a lattice $\alpha$ with a bottom element. The family $f$ is supremum independent on the attached set $s.\text{attach}$ (where each element is paired with its membership proof) if and only if $f$ is supremum independent on $s$.

Finset.supIndep_iff_pairwiseDisjoint theorem

: s.SupIndep f ↔ (s : Set ι).PairwiseDisjoint f

Full source

theorem supIndep_iff_pairwiseDisjoint : s.SupIndep f ↔ (s : Set ι).PairwiseDisjoint f :=
  ⟨SupIndep.pairwiseDisjoint, fun hs _ ht _ hi hit =>
    Finset.disjoint_sup_right.2 fun _ hj => hs hi (ht hj) (ne_of_mem_of_not_mem hj hit).symm⟩

Equivalence of Supremum Independence and Pairwise Disjointness in Finite Sets

Informal description

Let $s$ be a finite set and $f : \iota \to \alpha$ a family of elements in a distributive lattice $\alpha$ with a bottom element $\bot$. Then, the family $f$ is supremum independent on $s$ if and only if the family $f$ is pairwise disjoint on $s$, i.e., for any two distinct elements $i, j \in s$, the elements $f(i)$ and $f(j)$ are disjoint.

Finset.SupIndep.sup theorem

 [DecidableEq ι] {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α} (hs : s.SupIndep fun i => (g i).sup f)
  (hg : ∀ i' ∈ s, (g i').SupIndep f) : (s.sup g).SupIndep f

Full source

/-- Bind operation for `SupIndep`. -/
protected theorem SupIndep.sup [DecidableEq ι] {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α}
    (hs : s.SupIndep fun i => (g i).sup f) (hg : ∀ i' ∈ s, (g i').SupIndep f) :
    (s.sup g).SupIndep f := by
  simp_rw [supIndep_iff_pairwiseDisjoint] at hs hg ⊢
  rw [sup_eq_biUnion, coe_biUnion]
  exact hs.biUnion_finset hg

Supremum Independence Preservation under Finite Suprema

Informal description

Let $\alpha$ be a distributive lattice with a bottom element $\bot$, and let $s$ be a finite set of indices of type $\iota'$. Consider a family of finite sets $g : \iota' \to \text{Finset } \iota$ and a function $f : \iota \to \alpha$. If the family $\lambda i, \bigsqcup_{j \in g(i)} f(j)$ is supremum independent on $s$, and for each $i' \in s$, the family $f$ is supremum independent on $g(i')$, then $f$ is supremum independent on the finite set $\bigsqcup_{i' \in s} g(i')$.

Finset.SupIndep.biUnion theorem

 [DecidableEq ι] {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α} (hs : s.SupIndep fun i => (g i).sup f)
  (hg : ∀ i' ∈ s, (g i').SupIndep f) : (s.biUnion g).SupIndep f

Full source

/-- Bind operation for `SupIndep`. -/
protected theorem SupIndep.biUnion [DecidableEq ι] {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α}
    (hs : s.SupIndep fun i => (g i).sup f) (hg : ∀ i' ∈ s, (g i').SupIndep f) :
    (s.biUnion g).SupIndep f := by
  rw [← sup_eq_biUnion]
  exact hs.sup hg

Supremum Independence Preservation under Finite Union

Informal description

Let $\alpha$ be a distributive lattice with a bottom element $\bot$, and let $s$ be a finite set of indices of type $\iota'$. Consider a family of finite sets $g : \iota' \to \text{Finset } \iota$ and a function $f : \iota \to \alpha$. If the family $\lambda i, \bigsqcup_{j \in g(i)} f(j)$ is supremum independent on $s$, and for each $i' \in s$, the family $f$ is supremum independent on $g(i')$, then $f$ is supremum independent on the finite union $\bigcup_{i' \in s} g(i')$.

Finset.SupIndep.sigma theorem

 {β : ι → Type*} {s : Finset ι} {g : ∀ i, Finset (β i)} {f : Sigma β → α}
  (hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩) (hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩) :
  (s.sigma g).SupIndep f

Full source

/-- Bind operation for `SupIndep`. -/
protected theorem SupIndep.sigma {β : ι → Type*} {s : Finset ι} {g : ∀ i, Finset (β i)}
    {f : Sigma β → α} (hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩)
    (hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩) : (s.sigma g).SupIndep f := by
  rintro t ht ⟨i, b⟩ hi hit
  rw [Finset.disjoint_sup_right]
  rintro ⟨j, c⟩ hj
  have hbc := (ne_of_mem_of_not_mem hj hit).symm
  replace hj := ht hj
  rw [mem_sigma] at hi hj
  obtain rfl | hij := eq_or_ne i j
  · exact (hg _ hj.1).pairwiseDisjoint hi.2 hj.2 (sigma_mk_injective.ne_iff.1 hbc)
  · refine (hs.pairwiseDisjoint hi.1 hj.1 hij).mono ?_ ?_
    · convert le_sup (α := α) hi.2; simp
    · convert le_sup (α := α) hj.2; simp

Supremum Independence Preservation under Dependent Pair Construction

Informal description

Let $\beta$ be a family of types indexed by $\iota$, and let $s$ be a finite set of indices of type $\iota$. Consider a family of finite sets $g : \forall i \in \iota, \text{Finset } (\beta i)$ and a function $f : \Sigma i, \beta i \to \alpha$, where $\alpha$ is a lattice with a bottom element $\bot$. If the family $\lambda i, \bigsqcup_{b \in g(i)} f(i, b)$ is supremum independent on $s$, and for each $i \in s$, the family $\lambda b, f(i, b)$ is supremum independent on $g(i)$, then $f$ is supremum independent on the finite set $\Sigma i \in s, g(i)$.

Finset.SupIndep.product theorem

 {s : Finset ι} {t : Finset ι'} {f : ι × ι' → α} (hs : s.SupIndep fun i => t.sup fun i' => f (i, i'))
  (ht : t.SupIndep fun i' => s.sup fun i => f (i, i')) : (s ×ˢ t).SupIndep f

Full source

protected theorem SupIndep.product {s : Finset ι} {t : Finset ι'} {f : ι × ι' → α}
    (hs : s.SupIndep fun i => t.sup fun i' => f (i, i'))
    (ht : t.SupIndep fun i' => s.sup fun i => f (i, i')) : (s ×ˢ t).SupIndep f := by
  rintro u hu ⟨i, i'⟩ hi hiu
  rw [Finset.disjoint_sup_right]
  rintro ⟨j, j'⟩ hj
  have hij := (ne_of_mem_of_not_mem hj hiu).symm
  replace hj := hu hj
  rw [mem_product] at hi hj
  obtain rfl | hij := eq_or_ne i j
  · refine (ht.pairwiseDisjoint hi.2 hj.2 <| (Prod.mk_right_injective _).ne_iff.1 hij).mono ?_ ?_
    · convert le_sup (α := α) hi.1; simp
    · convert le_sup (α := α) hj.1; simp
  · refine (hs.pairwiseDisjoint hi.1 hj.1 hij).mono ?_ ?_
    · convert le_sup (α := α) hi.2; simp
    · convert le_sup (α := α) hj.2; simp

Supremum Independence of Product Sets

Informal description

Let $s$ be a finite set indexed by $\iota$, $t$ a finite set indexed by $\iota'$, and $f : \iota \times \iota' \to \alpha$ a family of elements in a lattice $\alpha$ with a bottom element $\bot$. If the family $i \mapsto \sup_{i' \in t} f(i, i')$ is supremum independent on $s$ and the family $i' \mapsto \sup_{i \in s} f(i, i')$ is supremum independent on $t$, then the family $f$ is supremum independent on the product set $s \times t$.

Finset.supIndep_product_iff theorem

 {s : Finset ι} {t : Finset ι'} {f : ι × ι' → α} :
  (s.product t).SupIndep f ↔
    (s.SupIndep fun i => t.sup fun i' => f (i, i')) ∧ t.SupIndep fun i' => s.sup fun i => f (i, i')

Full source

theorem supIndep_product_iff {s : Finset ι} {t : Finset ι'} {f : ι × ι' → α} :
    (s.product t).SupIndep f ↔ (s.SupIndep fun i => t.sup fun i' => f (i, i'))
      ∧ t.SupIndep fun i' => s.sup fun i => f (i, i') := by
  refine ⟨?_, fun h => h.1.product h.2⟩
  simp_rw [supIndep_iff_pairwiseDisjoint]
  refine fun h => ⟨fun i hi j hj hij => ?_, fun i hi j hj hij => ?_⟩ <;>
      simp_rw [Finset.disjoint_sup_left, Finset.disjoint_sup_right] <;>
    intro i' hi' j' hj'
  · exact h (mk_mem_product hi hi') (mk_mem_product hj hj') (ne_of_apply_ne Prod.fst hij)
  · exact h (mk_mem_product hi' hi) (mk_mem_product hj' hj) (ne_of_apply_ne Prod.snd hij)

Equivalence of Supremum Independence for Product Sets

Informal description

Let $s$ be a finite set indexed by $\iota$, $t$ a finite set indexed by $\iota'$, and $f : \iota \times \iota' \to \alpha$ a family of elements in a lattice $\alpha$ with a bottom element $\bot$. Then the following are equivalent: 1. The family $f$ is supremum independent on the product set $s \times t$. 2. The family $i \mapsto \sup_{i' \in t} f(i, i')$ is supremum independent on $s$ and the family $i' \mapsto \sup_{i \in s} f(i, i')$ is supremum independent on $t$.

sSupIndep definition

(s : Set α) : Prop

Full source

/-- An independent set of elements in a complete lattice is one in which every element is disjoint
  from the `Sup` of the rest. -/
def sSupIndep (s : Set α) : Prop :=
  ∀ ⦃a⦄, a ∈ s → Disjoint a (sSup (s \ {a}))

Supremum independent set

Informal description

A set $s$ in a complete lattice $\alpha$ is called *supremum independent* if for every element $a \in s$, the element $a$ is disjoint from the supremum of the remaining elements $s \setminus \{a\}$.

sSupIndep_empty theorem

: sSupIndep (∅ : Set α)

Full source

@[simp]
theorem sSupIndep_empty : sSupIndep (∅ : Set α) := fun x hx =>
  (Set.not_mem_empty x hx).elim

Empty Set is Supremum Independent

Informal description

The empty set is supremum independent in any complete lattice $\alpha$.

sSupIndep.mono theorem

{t : Set α} (hst : t ⊆ s) : sSupIndep t

Full source

theorem sSupIndep.mono {t : Set α} (hst : t ⊆ s) : sSupIndep t := fun _ ha =>
  (hs (hst ha)).mono_right (sSup_le_sSup (diff_subset_diff_left hst))

Subset of Supremum Independent Set is Supremum Independent

Informal description

Let $s$ be a supremum independent set in a complete lattice $\alpha$. For any subset $t \subseteq s$, the set $t$ is also supremum independent.

sSupIndep.pairwiseDisjoint theorem

: s.PairwiseDisjoint id

Full source

/-- If the elements of a set are independent, then any pair within that set is disjoint. -/
theorem sSupIndep.pairwiseDisjoint : s.PairwiseDisjoint id := fun _ hx y hy h =>
  disjoint_sSup_right (hs hx) ((mem_diff y).mpr ⟨hy, h.symm⟩)

Supremum independence implies pairwise disjointness

Informal description

For any set $s$ in a complete lattice $\alpha$, if $s$ is supremum independent, then the elements of $s$ are pairwise disjoint under the identity function. That is, for any two distinct elements $a, b \in s$, $a$ and $b$ are disjoint.

sSupIndep_singleton theorem

(a : α) : sSupIndep ({ a } : Set α)

Full source

theorem sSupIndep_singleton (a : α) : sSupIndep ({a} : Set α) := fun i hi ↦ by
  simp_all

Singleton sets are supremum independent

Informal description

For any element $a$ in a complete lattice $\alpha$, the singleton set $\{a\}$ is supremum independent. That is, $a$ is disjoint from the supremum of the empty set (which is $\bot$ in a complete lattice).

sSupIndep_pair theorem

{a b : α} (hab : a ≠ b) : sSupIndep ({ a, b } : Set α) ↔ Disjoint a b

Full source

theorem sSupIndep_pair {a b : α} (hab : a ≠ b) :
    sSupIndepsSupIndep ({a, b} : Set α) ↔ Disjoint a b := by
  constructor
  · intro h
    exact h.pairwiseDisjoint (mem_insert _ _) (mem_insert_of_mem _ (mem_singleton _)) hab
  · rintro h c ((rfl : c = a) | (rfl : c = b))
    · convert h using 1
      simp [hab, sSup_singleton]
    · convert h.symm using 1
      simp [hab, sSup_singleton]

Supremum Independence of Two Distinct Elements is Equivalent to Their Disjointness

Informal description

For any two distinct elements $a$ and $b$ in a complete lattice $\alpha$, the set $\{a, b\}$ is supremum independent if and only if $a$ and $b$ are disjoint. In other words, $\{a, b\}$ is supremum independent $\iff$ $a \sqcap b = \bot$.

sSupIndep.disjoint_sSup theorem

{x : α} {y : Set α} (hx : x ∈ s) (hy : y ⊆ s) (hxy : x ∉ y) : Disjoint x (sSup y)

Full source

/-- If the elements of a set are independent, then any element is disjoint from the `sSup` of some
subset of the rest. -/
theorem sSupIndep.disjoint_sSup {x : α} {y : Set α} (hx : x ∈ s) (hy : y ⊆ s) (hxy : x ∉ y) :
    Disjoint x (sSup y) := by
  have := (hs.mono <| insert_subset_iff.mpr ⟨hx, hy⟩) (mem_insert x _)
  rw [insert_diff_of_mem _ (mem_singleton _), diff_singleton_eq_self hxy] at this
  exact this

Disjointness of Element with Supremum of Subset in Supremum Independent Set

Informal description

Let $s$ be a supremum independent set in a complete lattice $\alpha$. For any element $x \in s$ and any subset $y \subseteq s$ such that $x \notin y$, the element $x$ is disjoint from the supremum of $y$, i.e., $x \sqcap \bigsqcup y = \bot$.

iSupIndep definition

{ι : Sort*} {α : Type*} [CompleteLattice α] (t : ι → α) : Prop

Full source

/-- An independent indexed family of elements in a complete lattice is one in which every element
  is disjoint from the `iSup` of the rest.

  Example: an indexed family of non-zero elements in a
  vector space is linearly independent iff the indexed family of subspaces they generate is
  independent in this sense.

  Example: an indexed family of submodules of a module is independent in this sense if
  and only the natural map from the direct sum of the submodules to the module is injective. -/
def iSupIndep {ι : Sort*} {α : Type*} [CompleteLattice α] (t : ι → α) : Prop :=
  ∀ i : ι, Disjoint (t i) (⨆ (j) (_ : j ≠ i), t j)

Supremum independent family

Informal description

An indexed family of elements $t : \iota \to \alpha$ in a complete lattice $\alpha$ is called *supremum independent* if for every index $i$, the element $t_i$ is disjoint from the supremum of all other elements in the family, i.e., $\text{Disjoint}(t_i, \bigsqcup_{j \neq i} t_j)$. This generalizes the notion of linear independence in vector spaces, where a family of vectors is linearly independent if and only if the family of subspaces they generate is supremum independent in this sense.

sSupIndep_iff theorem

{α : Type*} [CompleteLattice α] (s : Set α) : sSupIndep s ↔ iSupIndep ((↑) : s → α)

Full source

theorem sSupIndep_iff {α : Type*} [CompleteLattice α] (s : Set α) :
    sSupIndepsSupIndep s ↔ iSupIndep ((↑) : s → α) := by
  simp_rw [iSupIndep, sSupIndep, SetCoe.forall, sSup_eq_iSup]
  refine forall₂_congr fun a ha => ?_
  simp [iSup_subtype, iSup_and]

Equivalence of Set and Family Supremum Independence in Complete Lattices

Informal description

For a set $s$ in a complete lattice $\alpha$, $s$ is supremum independent if and only if the inclusion map from $s$ to $\alpha$ is supremum independent as an indexed family. That is, for every element $x \in s$, $x$ is disjoint from the supremum of the remaining elements $s \setminus \{x\}$ if and only if for every $x \in s$, $x$ is disjoint from the supremum of all other elements in $s$.

iSupIndep_def theorem

: iSupIndep t ↔ ∀ i, Disjoint (t i) (⨆ (j) (_ : j ≠ i), t j)

Full source

theorem iSupIndep_def : iSupIndepiSupIndep t ↔ ∀ i, Disjoint (t i) (⨆ (j) (_ : j ≠ i), t j) :=
  Iff.rfl

Characterization of Supremum Independent Families via Disjointness

Informal description

An indexed family of elements $t : \iota \to \alpha$ in a complete lattice $\alpha$ is supremum independent if and only if for every index $i$, the element $t_i$ is disjoint from the supremum of all other elements in the family, i.e., $\text{Disjoint}(t_i, \bigsqcup_{j \neq i} t_j)$.

iSupIndep_def' theorem

: iSupIndep t ↔ ∀ i, Disjoint (t i) (sSup (t '' {j | j ≠ i}))

Full source

theorem iSupIndep_def' : iSupIndepiSupIndep t ↔ ∀ i, Disjoint (t i) (sSup (t '' { j | j ≠ i })) := by
  simp_rw [sSup_image]
  rfl

Characterization of Supremum Independent Families via Disjointness

Informal description

An indexed family of elements $t : \iota \to \alpha$ in a complete lattice $\alpha$ is supremum independent if and only if for every index $i$, the element $t_i$ is disjoint from the supremum of the image of $t$ over all indices $j \neq i$. In other words, $\text{iSupIndep}\, t \leftrightarrow \forall i, \text{Disjoint}(t_i, \text{sSup}(t(\{j \mid j \neq i\})))$.

iSupIndep_def'' theorem

: iSupIndep t ↔ ∀ i, Disjoint (t i) (sSup {a | ∃ j ≠ i, t j = a})

Full source

theorem iSupIndep_def'' :
    iSupIndepiSupIndep t ↔ ∀ i, Disjoint (t i) (sSup { a | ∃ j ≠ i, t j = a }) := by
  rw [iSupIndep_def']
  aesop

Characterization of Supremum Independent Families via Disjointness with Supremum of Remaining Elements

Informal description

An indexed family of elements $t : \iota \to \alpha$ in a complete lattice $\alpha$ is supremum independent if and only if for every index $i$, the element $t_i$ is disjoint from the supremum of the set $\{a \mid \exists j \neq i, t_j = a\}$.

iSupIndep_empty theorem

(t : Empty → α) : iSupIndep t

Full source

@[simp]
theorem iSupIndep_empty (t : Empty → α) : iSupIndep t :=
  nofun

Supremum Independence of Empty Family

Informal description

For any complete lattice $\alpha$, any family of elements indexed by the empty type is supremum independent.

iSupIndep_pempty theorem

(t : PEmpty → α) : iSupIndep t

Full source

@[simp]
theorem iSupIndep_pempty (t : PEmpty → α) : iSupIndep t :=
  nofun

Supremum Independence of Empty Family

Informal description

For any complete lattice $\alpha$, any family of elements indexed by the empty type `PEmpty` is supremum independent.

iSupIndep.pairwiseDisjoint theorem

: Pairwise (Disjoint on t)

Full source

/-- If the elements of a set are independent, then any pair within that set is disjoint. -/
theorem iSupIndep.pairwiseDisjoint : Pairwise (DisjointDisjoint on t) := fun x y h =>
  disjoint_sSup_right (ht x) ⟨y, iSup_pos h.symm⟩

Supremum Independence Implies Pairwise Disjointness

Informal description

If a family of elements $t : \iota \to \alpha$ in a complete lattice $\alpha$ is supremum independent, then the elements are pairwise disjoint, i.e., for any two distinct indices $i$ and $j$, the elements $t(i)$ and $t(j)$ are disjoint.

iSupIndep.mono theorem

{s t : ι → α} (hs : iSupIndep s) (hst : t ≤ s) : iSupIndep t

Full source

theorem iSupIndep.mono {s t : ι → α} (hs : iSupIndep s) (hst : t ≤ s) : iSupIndep t :=
  fun i => (hs i).mono (hst i) <| iSup₂_mono fun j _ => hst j

Monotonicity of Supremum Independence: $t \leq s$ Preserves $\text{iSupIndep}$

Informal description

Let $\alpha$ be a complete lattice and $s, t : \iota \to \alpha$ be two indexed families of elements in $\alpha$. If $s$ is supremum independent and $t(i) \leq s(i)$ for all $i \in \iota$, then $t$ is also supremum independent.

iSupIndep.comp theorem

{ι ι' : Sort*} {t : ι → α} {f : ι' → ι} (ht : iSupIndep t) (hf : Injective f) : iSupIndep (t ∘ f)

Full source

/-- Composing an independent indexed family with an injective function on the index results in
another indepedendent indexed family. -/
theorem iSupIndep.comp {ι ι' : Sort*} {t : ι → α} {f : ι' → ι} (ht : iSupIndep t)
    (hf : Injective f) : iSupIndep (t ∘ f) := fun i =>
  (ht (f i)).mono_right <| by
    refine (iSup_mono fun i => ?_).trans (iSup_comp_le _ f)
    exact iSup_const_mono hf.ne

Supremum Independence is Preserved under Injective Reindexing

Informal description

Let $\alpha$ be a complete lattice and $t : \iota \to \alpha$ be a supremum independent family. For any injective function $f : \iota' \to \iota$, the composed family $t \circ f : \iota' \to \alpha$ is also supremum independent.

iSupIndep.comp' theorem

{ι ι' : Sort*} {t : ι → α} {f : ι' → ι} (ht : iSupIndep <| t ∘ f) (hf : Surjective f) : iSupIndep t

Full source

theorem iSupIndep.comp' {ι ι' : Sort*} {t : ι → α} {f : ι' → ι} (ht : iSupIndep <| t ∘ f)
    (hf : Surjective f) : iSupIndep t := by
  intro i
  obtain ⟨i', rfl⟩ := hf i
  rw [← hf.iSup_comp]
  exact (ht i').mono_right (biSup_mono fun j' hij => mt (congr_arg f) hij)

Supremum Independence Preserved Under Surjective Precomposition

Informal description

Let $\alpha$ be a complete lattice, $\iota$ and $\iota'$ be index types, $t : \iota \to \alpha$ be a family of elements in $\alpha$, and $f : \iota' \to \iota$ be a surjective function. If the composition $t \circ f$ is supremum independent, then $t$ is also supremum independent.

iSupIndep.sSupIndep_range theorem

(ht : iSupIndep t) : sSupIndep <| range t

Full source

theorem iSupIndep.sSupIndep_range (ht : iSupIndep t) : sSupIndep <| range t := by
  rw [sSupIndep_iff]
  rw [← coe_comp_rangeFactorization t] at ht
  exact ht.comp' surjective_onto_range

Range of a Supremum Independent Family is Supremum Independent

Informal description

Let $\alpha$ be a complete lattice and $t : \iota \to \alpha$ be a supremum independent family of elements. Then the range of $t$, $\text{range}(t) = \{t_i \mid i \in \iota\}$, is a supremum independent set in $\alpha$.

iSupIndep_ne_bot theorem

: iSupIndep (fun i : { i // t i ≠ ⊥ } ↦ t i) ↔ iSupIndep t

Full source

@[simp]
theorem iSupIndep_ne_bot :
    iSupIndepiSupIndep (fun i : {i // t i ≠ ⊥} ↦ t i) ↔ iSupIndep t := by
  refine ⟨fun h ↦ ?_, fun h ↦ h.comp Subtype.val_injective⟩
  simp only [iSupIndep_def] at h ⊢
  intro i
  cases eq_or_ne (t i) ⊥ with
  | inl hi => simp [hi]
  | inr hi => ?_
  convert h ⟨i, hi⟩
  have : ∀ j, ⨆ (_ : t j = ⊥), t j = ⊥ := fun j ↦ by simp only [iSup_eq_bot, imp_self]
  rw [iSup_split _ (fun j ↦ t j = ⊥), iSup_subtype]
  simp only [iSup_comm (ι' := _ ≠ i), this, ne_eq, sup_of_le_right, Subtype.mk.injEq, iSup_bot,
    bot_le]

Supremum Independence of Non-Bottom Elements is Equivalent to Full Supremum Independence

Informal description

Let $\alpha$ be a complete lattice and $t : \iota \to \alpha$ be a family of elements. The family $t$ is supremum independent if and only if the restriction of $t$ to the indices where $t_i \neq \bot$ is supremum independent. In other words, the supremum independence of $t$ is equivalent to the supremum independence of its non-bottom elements.

iSupIndep.injOn theorem

(ht : iSupIndep t) : InjOn t {i | t i ≠ ⊥}

Full source

theorem iSupIndep.injOn (ht : iSupIndep t) : InjOn t {i | t i ≠ ⊥} := by
  rintro i _ j (hj : t j ≠ ⊥) h
  by_contra! contra
  apply hj
  suffices t j ≤ ⨆ (k) (_ : k ≠ i), t k by
    replace ht := (ht i).mono_right this
    rwa [h, disjoint_self] at ht
  replace contra : j ≠ i := Ne.symm contra
  -- Porting note: needs explicit `f`
  exact le_iSup₂ (f := fun x _ ↦ t x) j contra

Injectivity of Supremum Independent Family on Non-Bottom Elements

Informal description

If a family of elements $t : \iota \to \alpha$ in a complete lattice $\alpha$ is supremum independent, then the function $t$ is injective on the subset $\{i \mid t_i \neq \bot\}$ of its domain. In other words, for any two distinct indices $i$ and $j$ where $t_i$ and $t_j$ are not the bottom element, we have $t_i \neq t_j$.

iSupIndep.injective theorem

(ht : iSupIndep t) (h_ne_bot : ∀ i, t i ≠ ⊥) : Injective t

Full source

theorem iSupIndep.injective (ht : iSupIndep t) (h_ne_bot : ∀ i, t i ≠ ⊥) : Injective t := by
  suffices univ = {i | t i ≠ ⊥} by rw [injective_iff_injOn_univ, this]; exact ht.injOn
  aesop

Injectivity of Supremum Independent Family with Non-Bottom Elements

Informal description

Let $\alpha$ be a complete lattice and $t : \iota \to \alpha$ be a supremum independent family of elements. If $t_i \neq \bot$ for every index $i$, then the function $t$ is injective.

iSupIndep_pair theorem

{i j : ι} (hij : i ≠ j) (huniv : ∀ k, k = i ∨ k = j) : iSupIndep t ↔ Disjoint (t i) (t j)

Full source

theorem iSupIndep_pair {i j : ι} (hij : i ≠ j) (huniv : ∀ k, k = i ∨ k = j) :
    iSupIndepiSupIndep t ↔ Disjoint (t i) (t j) := by
  constructor
  · exact fun h => h.pairwiseDisjoint hij
  · rintro h k
    obtain rfl | rfl := huniv k
    · refine h.mono_right (iSup_le fun i => iSup_le fun hi => Eq.le ?_)
      rw [(huniv i).resolve_left hi]
    · refine h.symm.mono_right (iSup_le fun j => iSup_le fun hj => Eq.le ?_)
      rw [(huniv j).resolve_right hj]

Supremum Independence for Two-Element Family is Equivalent to Disjointness

Informal description

For any two distinct indices $i$ and $j$ in $\iota$, and assuming that every index $k$ is either equal to $i$ or $j$, the family of elements $t : \iota \to \alpha$ in a complete lattice $\alpha$ is supremum independent if and only if the elements $t(i)$ and $t(j)$ are disjoint.

iSupIndep.map_orderIso theorem

 {ι : Sort*} {α β : Type*} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) {a : ι → α} (ha : iSupIndep a) :
  iSupIndep (f ∘ a)

Full source

/-- Composing an independent indexed family with an order isomorphism on the elements results in
another independent indexed family. -/
theorem iSupIndep.map_orderIso {ι : Sort*} {α β : Type*} [CompleteLattice α]
    [CompleteLattice β] (f : α ≃o β) {a : ι → α} (ha : iSupIndep a) : iSupIndep (f ∘ a) :=
  fun i => ((ha i).map_orderIso f).mono_right (f.monotone.le_map_iSup₂ _)

Order Isomorphism Preserves Supremum Independence: $f \circ a$ is supremum independent when $a$ is

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \simeq_o \beta$ be an order isomorphism. If $a : \iota \to \alpha$ is a supremum independent family in $\alpha$, then the composition $f \circ a : \iota \to \beta$ is also a supremum independent family in $\beta$.

iSupIndep_map_orderIso_iff theorem

 {ι : Sort*} {α β : Type*} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) {a : ι → α} :
  iSupIndep (f ∘ a) ↔ iSupIndep a

Full source

@[simp]
theorem iSupIndep_map_orderIso_iff {ι : Sort*} {α β : Type*} [CompleteLattice α]
    [CompleteLattice β] (f : α ≃o β) {a : ι → α} : iSupIndepiSupIndep (f ∘ a) ↔ iSupIndep a :=
  ⟨fun h =>
    have hf : f.symm ∘ f ∘ a = a := congr_arg (· ∘ a) f.left_inv.comp_eq_id
    hf ▸ h.map_orderIso f.symm,
    fun h => h.map_orderIso f⟩

Order Isomorphism Preserves Supremum Independence: $f \circ a$ is supremum independent if and only if $a$ is

Informal description

Let $\alpha$ and $\beta$ be complete lattices, and let $f : \alpha \simeq_o \beta$ be an order isomorphism. For any family of elements $a : \iota \to \alpha$, the composition $f \circ a : \iota \to \beta$ is supremum independent if and only if $a$ is supremum independent in $\alpha$.

iSupIndep.disjoint_biSup theorem

 {ι : Type*} {α : Type*} [CompleteLattice α] {t : ι → α} (ht : iSupIndep t) {x : ι} {y : Set ι} (hx : x ∉ y) :
  Disjoint (t x) (⨆ i ∈ y, t i)

Full source

/-- If the elements of a set are independent, then any element is disjoint from the `iSup` of some
subset of the rest. -/
theorem iSupIndep.disjoint_biSup {ι : Type*} {α : Type*} [CompleteLattice α] {t : ι → α}
    (ht : iSupIndep t) {x : ι} {y : Set ι} (hx : x ∉ y) : Disjoint (t x) (⨆ i ∈ y, t i) :=
  Disjoint.mono_right (biSup_mono fun _ hi => (ne_of_mem_of_not_mem hi hx :)) (ht x)

Disjointness in Supremum Independent Families: $t(x) \sqcap \bigsqcup_{i \in y} t(i) = \bot$ for $x \notin y$

Informal description

Let $\alpha$ be a complete lattice and $t : \iota \to \alpha$ be a supremum independent family. For any $x \in \iota$ and any subset $y \subseteq \iota$ such that $x \notin y$, the element $t(x)$ is disjoint from the supremum $\bigsqcup_{i \in y} t(i)$.

iSupIndep.of_coe_Iic_comp theorem

{ι : Sort*} {a : α} {t : ι → Set.Iic a} (ht : iSupIndep ((↑) ∘ t : ι → α)) : iSupIndep t

Full source

lemma iSupIndep.of_coe_Iic_comp {ι : Sort*} {a : α} {t : ι → Set.Iic a}
    (ht : iSupIndep ((↑) ∘ t : ι → α)) : iSupIndep t := by
  intro i x
  specialize ht i
  simp_rw [Function.comp_apply, ← Set.Iic.coe_iSup] at ht
  exact @ht x

Supremum Independence via Interval Restriction

Informal description

Let $\alpha$ be a complete lattice, $a \in \alpha$, and $t : \iota \to \mathrm{Iic}(a)$ be a family of elements in the interval $(-\infty, a]$. If the composition of $t$ with the inclusion map $\mathrm{Iic}(a) \hookrightarrow \alpha$ is supremum independent, then $t$ itself is supremum independent.

iSupIndep_iff_supIndep theorem

{s : Finset ι} {f : ι → α} : iSupIndep (f ∘ ((↑) : s → ι)) ↔ s.SupIndep f

Full source

theorem iSupIndep_iff_supIndep {s : Finset ι} {f : ι → α} :
    iSupIndepiSupIndep (f ∘ ((↑) : s → ι)) ↔ s.SupIndep f := by
  classical
    rw [Finset.supIndep_iff_disjoint_erase]
    refine Subtype.forall.trans (forall₂_congr fun a b => ?_)
    rw [Finset.sup_eq_iSup]
    congr! 1
    refine iSup_subtype.trans ?_
    congr! 1
    simp [iSup_and, @iSup_comm _ (_ ∈ s)]

Equivalence of Supremum Independence for Finite Restrictions and Finite Sets: $iSupIndep(f|_s) \leftrightarrow s.SupIndep(f)$

Informal description

Let $s$ be a finite set of indices and $f : \iota \to \alpha$ be a family of elements in a complete lattice $\alpha$. The family $f$ is supremum independent when restricted to $s$ (i.e., $i \mapsto f(i)$ for $i \in s$) if and only if the finite set $s$ is supremum independent with respect to $f$.

iSupIndep.supIndep' theorem

{f : ι → α} (s : Finset ι) (h : iSupIndep f) : s.SupIndep f

Full source

theorem iSupIndep.supIndep' {f : ι → α} (s : Finset ι) (h : iSupIndep f) : s.SupIndep f :=
  iSupIndep.supIndep (h.comp Subtype.coe_injective)

Supremum Independence Restricts to Finite Subsets

Informal description

Let $\alpha$ be a complete lattice and $f : \iota \to \alpha$ be a supremum independent family. For any finite subset $s \subseteq \iota$, the restriction of $f$ to $s$ is supremum independent on $s$.

iSupIndep_iff_supIndep_univ theorem

[Fintype ι] {f : ι → α} : iSupIndep f ↔ Finset.univ.SupIndep f

Full source

/-- A variant of `CompleteLattice.iSupIndep_iff_supIndep` for `Fintype`s. -/
theorem iSupIndep_iff_supIndep_univ [Fintype ι] {f : ι → α} :
    iSupIndepiSupIndep f ↔ Finset.univ.SupIndep f := by
  classical
    simp [Finset.supIndep_iff_disjoint_erase, iSupIndep, Finset.sup_eq_iSup]

Equivalence of Supremum Independence for Finite Types and Universal Finite Sets

Informal description

For a finite type $\iota$ and a family of elements $f : \iota \to \alpha$ in a complete lattice $\alpha$, the family $f$ is supremum independent if and only if it is supremum independent on the universal finite set $\mathrm{univ}$ (i.e., the entire index set $\iota$). In other words, the following are equivalent: 1. For every $i \in \iota$, the element $f(i)$ is disjoint from the supremum of the remaining elements $\bigsqcup_{j \neq i} f(j)$. 2. The family $f$ is supremum independent when restricted to the finite set $\mathrm{univ}$ (the entire $\iota$).

sSupIndep_iff_pairwiseDisjoint theorem

{s : Set α} : sSupIndep s ↔ s.PairwiseDisjoint id

Full source

theorem sSupIndep_iff_pairwiseDisjoint {s : Set α} : sSupIndepsSupIndep s ↔ s.PairwiseDisjoint id :=
  ⟨sSupIndep.pairwiseDisjoint, fun hs _ hi =>
    disjoint_sSup_iff.2 fun _ hj => hs hi hj.1 <| Ne.symm hj.2⟩

Equivalence of Supremum Independence and Pairwise Disjointness for Sets in Complete Lattices

Informal description

For any set $s$ in a complete lattice $\alpha$, the following are equivalent: 1. $s$ is supremum independent, meaning that for every element $a \in s$, $a$ is disjoint from the supremum of the remaining elements $\bigsqcup (s \setminus \{a\})$. 2. The elements of $s$ are pairwise disjoint under the identity function, meaning that for any two distinct elements $a, b \in s$, $a$ and $b$ are disjoint.

iSupIndep_iff_pairwiseDisjoint theorem

{f : ι → α} : iSupIndep f ↔ Pairwise (Disjoint on f)

Full source

theorem iSupIndep_iff_pairwiseDisjoint {f : ι → α} : iSupIndepiSupIndep f ↔ Pairwise (Disjoint on f) :=
  ⟨iSupIndep.pairwiseDisjoint, fun hs _ =>
    disjoint_iSup_iff.2 fun _ => disjoint_iSup_iff.2 fun hij => hs hij.symm⟩

Equivalence of Supremum Independence and Pairwise Disjointness in Complete Lattices

Informal description

For a family of elements $f : \iota \to \alpha$ in a complete lattice $\alpha$, the following are equivalent: 1. The family is supremum independent, meaning that for every index $i$, the element $f(i)$ is disjoint from the supremum of all other elements $\bigsqcup_{j \neq i} f(j)$. 2. The family is pairwise disjoint, meaning that for any two distinct indices $i$ and $j$, the elements $f(i)$ and $f(j)$ are disjoint.

Mathlib.Order.SupIndep

Main definitions

Main statements

Implementation notes