Finite 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.
In distributive lattices, this is equivalent to being pairwise disjoint.
Implementation notes #
We avoid the "obvious" definition ∀ i ∈ s, disjoint (f i) ((s.erase i).sup f)
because erase
would require decidable equality on ι
.
TODO #
complete_lattice.independent
and complete_lattice.set_independent
should live in this file.
Supremum independence of finite sets. We avoid the "obvious" definition usings.erase i
because
erase
would require decidable equality on ι
.
The RHS looks like the definition of complete_lattice.independent
.
Alias of sup_indep_iff_pairwise_disjoint
.
Bind operation for sup_indep
.
Bind operation for sup_indep
.