Lean4
/-- 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)
