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.

source

def finset.sup_indep {α : Type u_1} {ι : Type u_3} [lattice α] [order_bot α] (s : finset ι) (f : ι → α) :

Prop

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

Equations

s.sup_indep f = ∀ ⦃t : finset ι⦄, t ⊆ s → ∀ ⦃i : ι⦄, i ∈ s → i ∉ t → disjoint (f i) (t.sup f)

source

theorem finset.sup_indep.subset {α : Type u_1} {ι : Type u_3} [lattice α] [order_bot α] {s t : finset ι} {f : ι → α} (ht : t.sup_indep f) (h : s ⊆ t) :

s.sup_indep f

source

theorem finset.sup_indep_empty {α : Type u_1} {ι : Type u_3} [lattice α] [order_bot α] (f : ι → α) :

∅.sup_indep f

source

theorem finset.sup_indep_singleton {α : Type u_1} {ι : Type u_3} [lattice α] [order_bot α] (i : ι) (f : ι → α) :

{i}.sup_indep f

source

theorem finset.sup_indep.pairwise_disjoint {α : Type u_1} {ι : Type u_3} [lattice α] [order_bot α] {s : finset ι} {f : ι → α} (hs : s.sup_indep f) :

↑s.pairwise_disjoint f

source

theorem finset.sup_indep_iff_disjoint_erase {α : Type u_1} {ι : Type u_3} [lattice α] [order_bot α] {s : finset ι} {f : ι → α} [decidable_eq ι] :

s.sup_indep f ↔ ∀ (i : ι), i ∈ s → disjoint (f i) ((s.erase i).sup f)

The RHS looks like the definition of complete_lattice.independent.

source

theorem finset.sup_indep.attach {α : Type u_1} {ι : Type u_3} [lattice α] [order_bot α] {s : finset ι} {f : ι → α} (hs : s.sup_indep f) :

s.attach.sup_indep (f ∘ subtype.val)

source

theorem finset.sup_indep_iff_pairwise_disjoint {α : Type u_1} {ι : Type u_3} [distrib_lattice α] [order_bot α] {s : finset ι} {f : ι → α} :

s.sup_indep f ↔ ↑s.pairwise_disjoint f

source

theorem set.pairwise_disjoint.sup_indep {α : Type u_1} {ι : Type u_3} [distrib_lattice α] [order_bot α] {s : finset ι} {f : ι → α} :

↑s.pairwise_disjoint f → s.sup_indep f

Alias of sup_indep_iff_pairwise_disjoint.

source

theorem finset.sup_indep.sup {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [distrib_lattice α] [order_bot α] [decidable_eq ι] {s : finset ι'} {g : ι' → finset ι} {f : ι → α} (hs : s.sup_indep (λ (i : ι'), (g i).sup f)) (hg : ∀ (i' : ι'), i' ∈ s → (g i').sup_indep f) :

(s.sup g).sup_indep f

Bind operation for sup_indep.

source

theorem finset.sup_indep.bUnion {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [distrib_lattice α] [order_bot α] [decidable_eq ι] {s : finset ι'} {g : ι' → finset ι} {f : ι → α} (hs : s.sup_indep (λ (i : ι'), (g i).sup f)) (hg : ∀ (i' : ι'), i' ∈ s → (g i').sup_indep f) :

(s.bUnion g).sup_indep f

Bind operation for sup_indep.

source

theorem complete_lattice.independent_iff_sup_indep {α : Type u_1} {ι : Type u_3} [complete_lattice α] {s : finset ι} {f : ι → α} :

complete_lattice.independent (f ∘ coe) ↔ s.sup_indep f

source

theorem complete_lattice.independent.sup_indep {α : Type u_1} {ι : Type u_3} [complete_lattice α] {s : finset ι} {f : ι → α} :

complete_lattice.independent (f ∘ coe) → s.sup_indep f

Alias of complete_lattice.independent_iff_sup_indep.

source

theorem finset.sup_indep.independent {α : Type u_1} {ι : Type u_3} [complete_lattice α] {s : finset ι} {f : ι → α} :

s.sup_indep f → complete_lattice.independent (f ∘ coe)

Alias of complete_lattice.independent_iff_sup_indep.