# Supremum independence #

In this file, we define supremum independence of indexed sets. An indexed family `f : ι → α` is sup-independent if, for all `a`, `f a` and the supremum of the rest are disjoint.

## Main definitions #

- `Finset.SupIndep s f`: a family of elements `f` are supremum independent on the finite set `s`.
- `sSupIndep s`: a set of elements are supremum independent.
- `iSupIndep f`: a family of elements are supremum independent.

## Main statements #

- In a distributive lattice, supremum independence is equivalent to pairwise disjointness:
  - `Finset.supIndep_iff_pairwiseDisjoint`
  - `CompleteLattice.sSupIndep_iff_pairwiseDisjoint`
  - `CompleteLattice.iSupIndep_iff_pairwiseDisjoint`
- Otherwise, supremum independence is stronger than pairwise disjointness:
  - `Finset.SupIndep.pairwiseDisjoint`
  - `sSupIndep.pairwiseDisjoint`
  - `iSupIndep.pairwiseDisjoint`

## Implementation notes #

For the finite version, we avoid the "obvious" definition `∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)` because `erase` would require decidable equality on `ι`.

### On lattices with a bottom element, via `Finset.sup` #

source
def Finset.SupIndep {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] (s : Finset ι) (f : ι → α) :
Prop

Supremum independence of finite sets. We avoid the "obvious" definition using `s.erase i` because `erase` would require decidable equality on `ι`.

Equations

- s.SupIndep f = ∀ ⦃t : Finset ι⦄, t ⊆ s → ∀ ⦃i : ι⦄, i ∈ s → i ∉ t → Disjoint (f i) (t.sup f)

Instances For

source
theorem Finset.supIndep_iff_disjoint_erase {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {f : ι → α} [DecidableEq ι] :
s.SupIndep f ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)

The RHS looks like the definition of `iSupIndep`.

source
instance Finset.instDecidableSupIndepOfDecidableEq {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {f : ι → α} [DecidableEq ι] [DecidableEq α] :
Decidable (s.SupIndep f)

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.

Equations

- Finset.instDecidableSupIndepOfDecidableEq = decidable_of_iff (∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)) ⋯

source
theorem Finset.SupIndep.subset {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s t : Finset ι} {f : ι → α} (ht : t.SupIndep f) (h : s ⊆ t) :
s.SupIndep f
source
theorem Finset.SupIndep.mono {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {f g : ι → α} (hf : s.SupIndep f) (h : ∀ i ∈ s, g i ≤ f i) :
s.SupIndep g
source
@[simp]
theorem Finset.supIndep_empty {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] (f : ι → α) :
∅.SupIndep f
source
@[simp]
theorem Finset.supIndep_singleton {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] (i : ι) (f : ι → α) :
{i}.SupIndep f
source
theorem Finset.SupIndep.pairwiseDisjoint {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {f : ι → α} (hs : s.SupIndep f) :
(↑s).PairwiseDisjoint f
source
theorem Finset.SupIndep.le_sup_iff {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s t : Finset ι} {f : ι → α} {i : ι} (hs : s.SupIndep f) (hts : t ⊆ s) (hi : i ∈ s) (hf : ∀ (i : ι), f i ≠ ⊥) :
f i ≤ t.sup f ↔ i ∈ t
source
theorem Finset.SupIndep.antitone_fun {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {f g : ι → α} (hle : ∀ x ∈ s, f x ≤ g x) (h : s.SupIndep g) :
s.SupIndep f
source
theorem Finset.SupIndep.image {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [Lattice α] [OrderBot α] {f : ι → α} [DecidableEq ι] {s : Finset ι'} {g : ι' → ι} (hs : s.SupIndep (f ∘ g)) :
(image g s).SupIndep f
source
theorem Finset.supIndep_map {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [Lattice α] [OrderBot α] {f : ι → α} {s : Finset ι'} {g : ι' ↪ ι} :
(map g s).SupIndep f ↔ s.SupIndep (f ∘ ⇑g)
source
@[simp]
theorem Finset.supIndep_pair {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {f : ι → α} [DecidableEq ι] {i j : ι} (hij : i ≠ j) :
{i, j}.SupIndep f ↔ Disjoint (f i) (f j)
source
theorem Finset.supIndep_univ_bool {α : Type u_1} [Lattice α] [OrderBot α] (f : Bool → α) :
univ.SupIndep f ↔ Disjoint (f false) (f true)
source
@[simp]
theorem Finset.supIndep_univ_fin_two {α : Type u_1} [Lattice α] [OrderBot α] (f : Fin 2 → α) :
univ.SupIndep f ↔ Disjoint (f 0) (f 1)
source
@[simp]
theorem Finset.supIndep_attach {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {f : ι → α} :
(s.attach.SupIndep fun (a : { x : ι // x ∈ s }) => f ↑a) ↔ s.SupIndep f
source
theorem Finset.SupIndep.attach {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {f : ι → α} :
s.SupIndep f → s.attach.SupIndep fun (a : { x : ι // x ∈ s }) => f ↑a

Alias of the reverse direction of `Finset.supIndep_attach`.

source
theorem Finset.SupIndep.biUnion {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [Lattice α] [IsModularLattice α] [OrderBot α] [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

Bind operation for `SupIndep`.

source
theorem Finset.SupIndep.sup {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [Lattice α] [IsModularLattice α] [OrderBot α] [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

Bind operation for `SupIndep`.

source
theorem Finset.SupIndep.sigma {α : Type u_1} {ι : Type u_3} [Lattice α] [IsModularLattice α] [OrderBot α] {β : ι → Type u_5} {s : Finset ι} {g : (i : ι) → Finset (β i)} {f : Sigma β → α} (hs : s.SupIndep fun (i : ι) => (g i).sup fun (b : β i) => f ⟨i, b⟩) (hg : ∀ i ∈ s, (g i).SupIndep fun (b : β i) => f ⟨i, b⟩) :
(s.sigma g).SupIndep f

Bind operation for `SupIndep`.

source
theorem Finset.SupIndep.product {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [Lattice α] [IsModularLattice α] [OrderBot α] {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
source
theorem Finset.SupIndep.disjoint_sup_sup {α : Type u_1} {ι : Type u_3} [Lattice α] [IsModularLattice α] [OrderBot α] {s : Finset ι} {f : ι → α} {u v : Finset ι} (hs : s.SupIndep f) (hu : u ⊆ s) (hv : v ⊆ s) (huv : Disjoint u v) :
Disjoint (u.sup f) (v.sup f)
source
theorem Finset.supIndep_sigma_iff' {α : Type u_1} {ι : Type u_3} [Lattice α] [IsModularLattice α] [OrderBot α] {β : ι → Type u_5} {s : Finset ι} {g : (i : ι) → Finset (β i)} {f : Sigma β → α} :
(s.sigma g).SupIndep f ↔ (s.SupIndep fun (i : ι) => (g i).sup fun (b : β i) => f ⟨i, b⟩) ∧ ∀ i ∈ s, (g i).SupIndep fun (b : β i) => f ⟨i, b⟩
source
theorem Finset.supIndep_product_iff {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [Lattice α] [IsModularLattice α] [OrderBot α] {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')
source
theorem Finset.supIndep_iff_pairwiseDisjoint {α : Type u_1} {ι : Type u_3} [DistribLattice α] [OrderBot α] {s : Finset ι} {f : ι → α} :
s.SupIndep f ↔ (↑s).PairwiseDisjoint f
source
theorem Set.PairwiseDisjoint.supIndep {α : Type u_1} {ι : Type u_3} [DistribLattice α] [OrderBot α] {s : Finset ι} {f : ι → α} :
(↑s).PairwiseDisjoint f → s.SupIndep f

Alias of the reverse direction of `Finset.supIndep_iff_pairwiseDisjoint`.

### On complete lattices via `sSup` #

source
def sSupIndep {α : Type u_1} [CompleteLattice α] (s : Set α) :
Prop

An independent set of elements in a complete lattice is one in which every element is disjoint from the `Sup` of the rest.

Equations

- sSupIndep s = ∀ ⦃a : α⦄, a ∈ s → Disjoint a (sSup (s \ {a}))

Instances For

source
@[simp]
theorem sSupIndep_empty {α : Type u_1} [CompleteLattice α] :
sSupIndep ∅
source
theorem sSupIndep.mono {α : Type u_1} [CompleteLattice α] {s : Set α} (hs : sSupIndep s) {t : Set α} (hst : t ⊆ s) :
sSupIndep t
source
theorem sSupIndep.pairwiseDisjoint {α : Type u_1} [CompleteLattice α] {s : Set α} (hs : sSupIndep s) :
s.PairwiseDisjoint id

If the elements of a set are independent, then any pair within that set is disjoint.

source
theorem sSupIndep_singleton {α : Type u_1} [CompleteLattice α] (a : α) :
sSupIndep {a}
source
theorem sSupIndep_pair {α : Type u_1} [CompleteLattice α] {a b : α} (hab : a ≠ b) :
sSupIndep {a, b} ↔ Disjoint a b
source
theorem sSupIndep.disjoint_sSup {α : Type u_1} [CompleteLattice α] {s : Set α} (hs : sSupIndep s) {x : α} {y : Set α} (hx : x ∈ s) (hy : y ⊆ s) (hxy : x ∉ y) :
Disjoint x (sSup y)

If the elements of a set are independent, then any element is disjoint from the `sSup` of some subset of the rest.

source
def iSupIndep {ι : Sort u_5} {α : Type u_6} [CompleteLattice α] (t : ι → α) :
Prop

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.

Equations

- iSupIndep t = ∀ (i : ι), Disjoint (t i) (⨆ (j : ι), ⨆ (_ : j ≠ i), t j)

Instances For

source
theorem sSupIndep_iff {α : Type u_5} [CompleteLattice α] (s : Set α) :
sSupIndep s ↔ iSupIndep Subtype.val
source
theorem iSupIndep_def {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ι → α} :
iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (⨆ (j : ι), ⨆ (_ : j ≠ i), t j)
source
theorem iSupIndep_def' {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ι → α} :
iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (sSup (t '' {j : ι | j ≠ i}))
source
theorem iSupIndep_def'' {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ι → α} :
iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (sSup {a : α | ∃ (j : ι), j ≠ i ∧ t j = a})
source
@[simp]
theorem iSupIndep_subsingleton {α : Type u_1} {ι : Type u_3} [CompleteLattice α] [Subsingleton ι] (t : ι → α) :
iSupIndep t
source
@[deprecated "use iSupIndep_subsingleton instead" (since := "2025-09-18")]
theorem iSupIndep_empty {α : Type u_1} [CompleteLattice α] (t : Empty → α) :
iSupIndep t
source
@[deprecated "use iSupIndep_subsingleton instead" (since := "2025-09-18")]
theorem iSupIndep_pempty {α : Type u_1} [CompleteLattice α] (t : PEmpty.{u_5} → α) :
iSupIndep t
source
theorem iSupIndep.pairwiseDisjoint {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ι → α} (ht : iSupIndep t) :
Pairwise (Function.onFun Disjoint t)

If the elements of a set are independent, then any pair within that set is disjoint.

source
theorem iSupIndep.mono {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {s t : ι → α} (hs : iSupIndep s) (hst : t ≤ s) :
iSupIndep t
source
theorem iSupIndep.comp {α : Type u_1} [CompleteLattice α] {ι : Sort u_5} {ι' : Sort u_6} {t : ι → α} {f : ι' → ι} (ht : iSupIndep t) (hf : Function.Injective f) :
iSupIndep (t ∘ f)

Composing an independent indexed family with an injective function on the index results in another independent indexed family.

source
theorem iSupIndep.comp' {α : Type u_1} [CompleteLattice α] {ι : Sort u_5} {ι' : Sort u_6} {t : ι → α} {f : ι' → ι} (ht : iSupIndep (t ∘ f)) (hf : Function.Surjective f) :
iSupIndep t
source
theorem iSupIndep.sSupIndep_range {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ι → α} (ht : iSupIndep t) :
sSupIndep (Set.range t)
source
@[simp]
theorem iSupIndep_ne_bot {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ι → α} :
(iSupIndep fun (i : { i : ι // t i ≠ ⊥ }) => t ↑i) ↔ iSupIndep t
source
theorem iSupIndep.injOn {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ι → α} (ht : iSupIndep t) :
Set.InjOn t {i : ι | t i ≠ ⊥}
source
theorem iSupIndep.injOn_iInf {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {β : ι → Type u_5} (t : (i : ι) → β i → α) (ht : ∀ (i : ι), iSupIndep (t i)) :
Set.InjOn (fun (b : (i : ι) → β i) => ⨅ (i : ι), t i (b i)) {b : (i : ι) → β i | ⨅ (i : ι), t i (b i) ≠ ⊥}
source
theorem iSupIndep.injective {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ι → α} (ht : iSupIndep t) (h_ne_bot : ∀ (i : ι), t i ≠ ⊥) :
Function.Injective t
source
theorem iSupIndep_pair {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ι → α} {i j : ι} (hij : i ≠ j) (huniv : ∀ (k : ι), k = i ∨ k = j) :
iSupIndep t ↔ Disjoint (t i) (t j)
source
theorem iSupIndep.map_orderIso {ι : Sort u_5} {α : Type u_6} {β : Type u_7} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) {a : ι → α} (ha : iSupIndep a) :
iSupIndep (⇑f ∘ a)

Composing an independent indexed family with an order isomorphism on the elements results in another independent indexed family.

source
@[simp]
theorem iSupIndep_map_orderIso_iff {ι : Sort u_5} {α : Type u_6} {β : Type u_7} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) {a : ι → α} :
iSupIndep (⇑f ∘ a) ↔ iSupIndep a
source
theorem iSupIndep.disjoint_biSup {ι : Type u_5} {α : Type u_6} [CompleteLattice α] {t : ι → α} (ht : iSupIndep t) {x : ι} {y : Set ι} (hx : x ∉ y) :
Disjoint (t x) (⨆ i ∈ y, t i)

If the elements of a set are independent, then any element is disjoint from the `iSup` of some subset of the rest.

source
theorem iSupIndep.of_coe_Iic_comp {α : Type u_1} [CompleteLattice α] {ι : Sort u_5} {a : α} {t : ι → ↑(Set.Iic a)} (ht : iSupIndep (Subtype.val ∘ t)) :
iSupIndep t
source
theorem iSupIndep_iff_supIndep {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {s : Finset ι} {f : ι → α} :
iSupIndep (f ∘ Subtype.val) ↔ s.SupIndep f
source
theorem Finset.SupIndep.independent {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {s : Finset ι} {f : ι → α} :
s.SupIndep f → iSupIndep (f ∘ Subtype.val)

Alias of the reverse direction of `iSupIndep_iff_supIndep`.

source
theorem iSupIndep.supIndep {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {s : Finset ι} {f : ι → α} :
iSupIndep (f ∘ Subtype.val) → s.SupIndep f

Alias of the forward direction of `iSupIndep_iff_supIndep`.

source
theorem iSupIndep.supIndep' {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {f : ι → α} (s : Finset ι) (h : iSupIndep f) :
s.SupIndep f
source
theorem iSupIndep_iff_supIndep_univ {α : Type u_1} {ι : Type u_3} [CompleteLattice α] [Fintype ι] {f : ι → α} :
iSupIndep f ↔ Finset.univ.SupIndep f

A variant of `CompleteLattice.iSupIndep_iff_supIndep` for `Fintype`s.

source
theorem iSupIndep.sup_indep_univ {α : Type u_1} {ι : Type u_3} [CompleteLattice α] [Fintype ι] {f : ι → α} :
iSupIndep f → Finset.univ.SupIndep f

Alias of the forward direction of `iSupIndep_iff_supIndep_univ`.

A variant of `CompleteLattice.iSupIndep_iff_supIndep` for `Fintype`s.

source
theorem Finset.SupIndep.iSupIndep_of_univ {α : Type u_1} {ι : Type u_3} [CompleteLattice α] [Fintype ι] {f : ι → α} :
univ.SupIndep f → iSupIndep f

Alias of the reverse direction of `iSupIndep_iff_supIndep_univ`.

A variant of `CompleteLattice.iSupIndep_iff_supIndep` for `Fintype`s.

source
theorem sSupIndep_iff_pairwiseDisjoint {α : Type u_1} [Order.Frame α] {s : Set α} :
sSupIndep s ↔ s.PairwiseDisjoint id
source
theorem Set.PairwiseDisjoint.sSupIndep {α : Type u_1} [Order.Frame α] {s : Set α} :
s.PairwiseDisjoint id → _root_.sSupIndep s

Alias of the reverse direction of `sSupIndep_iff_pairwiseDisjoint`.

source
theorem iSupIndep_iff_pairwiseDisjoint {α : Type u_1} {ι : Type u_3} [Order.Frame α] {f : ι → α} :
iSupIndep f ↔ Pairwise (Function.onFun Disjoint f)