Theorems · Definition · order theory

iSupIndep

{ι : Sort u_5} → {α : Type u_6} → [CompleteLattice α] → (ι → α) → 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.

Defined in

Mathlib.Order.SupIndep

Cited by

100 results in Mathlib

Foundations

Depth 10 from the axioms, rests on 74 definitions · uses no axioms

Assumes

CompleteLattice