Supremum-independent families

This file develops the API for supremum-independent families. The complement results turn an independent spanning family into complementary summands, enabling projections or retractions onto individual members.

Main declarations

• Finset.SupIndep.isCompl_sup_erase: a member of an independent finite family spanning a bounded lattice is complemented by the supremum of the other members.
• iSupIndep.isCompl_biSup_ne: a member of an independent family spanning a complete lattice is complemented by the supremum of the other members.

theorem Finset.SupIndep.isCompl_sup_erase {ι : Type u_1} {L : Type u_2} [Lattice L] [BoundedOrder L] [DecidableEq ι] {s : Finset ι} {f : ι → L} (hind : s.SupIndep f) (htop : s.sup f = ⊤) {i : ι} (hi : i ∈ s) : IsCompl (f i) ((s.erase i).sup f)

In a bounded lattice, a member of an independent finite family whose supremum is ⊤ is complemented by the supremum of the remaining members.

theorem iSupIndep.isCompl_biSup_ne {ι : Type u_1} {L : Type u_2} [CompleteLattice L] {f : ι → L} (hind : iSupIndep f) (htop : ⨆ (i : ι), f i = ⊤) (i : ι) : IsCompl (f i) (⨆ (j : ι), ⨆ (_ : j ≠ i), f j)

In a complete lattice, a member of an independent family whose supremum is ⊤ is complemented by the supremum of the remaining members.