mathlib3 documentation

order.sup_indep

Supremum independence #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

Main definitions #

finset.sup_indep s f: a family of elements f are supremum independent on the finite set s.
complete_lattice.set_independent s: a set of elements are supremum independent.
complete_lattice.independent f: a family of elements are supremum independent.

Main statements #

In a distributive lattice, supremum independence is equivalent to pairwise disjointness:
Otherwise, supremum independence is stronger than pairwise disjointness:

Implementation notes #

For the finite version, we avoid the "obvious" definition ∀ i ∈ s, disjoint (f i) ((s.erase i).sup f) because erase would require decidable equality on ι.

On lattices with a bottom element, via `finset.sup` #

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 using s.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)

Instances for finset.sup_indep

finset.sup_indep.decidable

@[protected, instance]

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

decidable (s.sup_indep f)

Equations

finset.sup_indep.decidable = finset.decidable_forall_of_decidable_subsets

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) :

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

∅.sup_indep f

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

{i}.sup_indep f

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

theorem finset.sup_indep.le_sup_iff {α : Type u_1} {ι : Type u_3} [lattice α] [order_bot α] {s t : finset ι} {f : ι → α} {i : ι} (hs : s.sup_indep f) (hts : t ⊆ s) (hi : i ∈ s) (hf : ∀ (i : ι), f i ≠ ⊥) :

f i ≤ t.sup f ↔ i ∈ t

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.

theorem finset.sup_indep.image {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [lattice α] [order_bot α] {f : ι → α} [decidable_eq ι] {s : finset ι'} {g : ι' → ι} (hs : s.sup_indep (f ∘ g)) :

(finset.image g s).sup_indep f

theorem finset.sup_indep_map {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [lattice α] [order_bot α] {f : ι → α} {s : finset ι'} {g : ι' ↪ ι} :

(finset.map g s).sup_indep f ↔ s.sup_indep (f ∘ ⇑g)

@[simp]

theorem finset.sup_indep_pair {α : Type u_1} {ι : Type u_3} [lattice α] [order_bot α] {f : ι → α} [decidable_eq ι] {i j : ι} (hij : i ≠ j) :

{i, j}.sup_indep f ↔ disjoint (f i) (f j)

theorem finset.sup_indep_univ_bool {α : Type u_1} [lattice α] [order_bot α] (f : bool → α) :

finset.univ.sup_indep f ↔ disjoint (f bool.ff) (f bool.tt)

@[simp]

theorem finset.sup_indep_univ_fin_two {α : Type u_1} [lattice α] [order_bot α] (f : fin 2 → α) :

finset.univ.sup_indep f ↔ disjoint (f 0) (f 1)

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 (λ (a : {x // x ∈ s}), f ↑a)

@[simp]

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

s.attach.sup_indep (λ (a : {x // x ∈ s}), f ↑a) ↔ s.sup_indep f

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

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 the reverse direction of finset.sup_indep_iff_pairwise_disjoint.

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.

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.

theorem finset.sup_indep.sigma {α : Type u_1} {ι : Type u_3} [distrib_lattice α] [order_bot α] {β : ι → Type u_2} {s : finset ι} {g : Π (i : ι), finset (β i)} {f : sigma β → α} (hs : s.sup_indep (λ (i : ι), (g i).sup (λ (b : β i), f ⟨i, b⟩))) (hg : ∀ (i : ι), i ∈ s → (g i).sup_indep (λ (b : β i), f ⟨i, b⟩)) :

(s.sigma g).sup_indep f

Bind operation for sup_indep.

theorem finset.sup_indep.product {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [distrib_lattice α] [order_bot α] {s : finset ι} {t : finset ι'} {f : ι × ι' → α} (hs : s.sup_indep (λ (i : ι), t.sup (λ (i' : ι'), f (i, i')))) (ht : t.sup_indep (λ (i' : ι'), s.sup (λ (i : ι), f (i, i')))) :

(s ×ˢ t).sup_indep f

theorem finset.sup_indep_product_iff {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [distrib_lattice α] [order_bot α] {s : finset ι} {t : finset ι'} {f : ι × ι' → α} :

(s ×ˢ t).sup_indep f ↔ s.sup_indep (λ (i : ι), t.sup (λ (i' : ι'), f (i, i'))) ∧ t.sup_indep (λ (i' : ι'), s.sup (λ (i : ι), f (i, i')))

On complete lattices via `has_Sup.Sup` #

def complete_lattice.set_independent {α : Type u_1} [complete_lattice α] (s : set α) :

Prop

An independent set of elements in a complete lattice is one in which every element is disjoint from the Sup of the rest.

Equations

complete_lattice.set_independent s = ∀ ⦃a : α⦄, a ∈ s → disjoint a (has_Sup.Sup (s \ {a}))

@[simp]

theorem complete_lattice.set_independent_empty {α : Type u_1} [complete_lattice α] :

complete_lattice.set_independent ∅

theorem complete_lattice.set_independent.mono {α : Type u_1} [complete_lattice α] {s : set α} (hs : complete_lattice.set_independent s) {t : set α} (hst : t ⊆ s) :

complete_lattice.set_independent t

theorem complete_lattice.set_independent.pairwise_disjoint {α : Type u_1} [complete_lattice α] {s : set α} (hs : complete_lattice.set_independent s) :

s.pairwise_disjoint id

If the elements of a set are independent, then any pair within that set is disjoint.

theorem complete_lattice.set_independent_pair {α : Type u_1} [complete_lattice α] {a b : α} (hab : a ≠ b) :

complete_lattice.set_independent {a, b} ↔ disjoint a b

theorem complete_lattice.set_independent.disjoint_Sup {α : Type u_1} [complete_lattice α] {s : set α} (hs : complete_lattice.set_independent s) {x : α} {y : set α} (hx : x ∈ s) (hy : y ⊆ s) (hxy : x ∉ y) :

disjoint x (has_Sup.Sup y)

If the elements of a set are independent, then any element is disjoint from the Sup of some subset of the rest.

def complete_lattice.independent {ι : Sort u_1} {α : Type u_2} [complete_lattice α] (t : ι → α) :

Prop

An independent indexed family of elements in a complete lattice is one in which every element is disjoint from the supr 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.

Equations

complete_lattice.independent t = ∀ (i : ι), disjoint (t i) (⨆ (j : ι) (H : j ≠ i), t j)

theorem complete_lattice.set_independent_iff {α : Type u_1} [complete_lattice α] (s : set α) :

complete_lattice.set_independent s ↔ complete_lattice.independent coe

theorem complete_lattice.independent_def {α : Type u_1} {ι : Type u_3} [complete_lattice α] {t : ι → α} :

complete_lattice.independent t ↔ ∀ (i : ι), disjoint (t i) (⨆ (j : ι) (H : j ≠ i), t j)

theorem complete_lattice.independent_def' {α : Type u_1} {ι : Type u_3} [complete_lattice α] {t : ι → α} :

complete_lattice.independent t ↔ ∀ (i : ι), disjoint (t i) (has_Sup.Sup (t '' {j : ι | j ≠ i}))

theorem complete_lattice.independent_def'' {α : Type u_1} {ι : Type u_3} [complete_lattice α] {t : ι → α} :

complete_lattice.independent t ↔ ∀ (i : ι), disjoint (t i) (has_Sup.Sup {a : α | ∃ (j : ι) (H : j ≠ i), t j = a})

@[simp]

theorem complete_lattice.independent_empty {α : Type u_1} [complete_lattice α] (t : empty → α) :

complete_lattice.independent t

@[simp]

theorem complete_lattice.independent_pempty {α : Type u_1} [complete_lattice α] (t : pempty → α) :

complete_lattice.independent t

theorem complete_lattice.independent.pairwise_disjoint {α : Type u_1} {ι : Type u_3} [complete_lattice α] {t : ι → α} (ht : complete_lattice.independent t) :

pairwise (disjoint on t)

If the elements of a set are independent, then any pair within that set is disjoint.

theorem complete_lattice.independent.mono {α : Type u_1} {ι : Type u_3} [complete_lattice α] {s t : ι → α} (hs : complete_lattice.independent s) (hst : t ≤ s) :

complete_lattice.independent t

theorem complete_lattice.independent.comp {α : Type u_1} [complete_lattice α] {ι : Sort u_2} {ι' : Sort u_3} {t : ι → α} {f : ι' → ι} (ht : complete_lattice.independent t) (hf : function.injective f) :

complete_lattice.independent (t ∘ f)

Composing an independent indexed family with an injective function on the index results in another indepedendent indexed family.

theorem complete_lattice.independent.comp' {α : Type u_1} [complete_lattice α] {ι : Sort u_2} {ι' : Sort u_3} {t : ι → α} {f : ι' → ι} (ht : complete_lattice.independent (t ∘ f)) (hf : function.surjective f) :

complete_lattice.independent t

theorem complete_lattice.independent.set_independent_range {α : Type u_1} {ι : Type u_3} [complete_lattice α] {t : ι → α} (ht : complete_lattice.independent t) :

complete_lattice.set_independent (set.range t)

theorem complete_lattice.independent.injective {α : Type u_1} {ι : Type u_3} [complete_lattice α] {t : ι → α} (ht : complete_lattice.independent t) (h_ne_bot : ∀ (i : ι), t i ≠ ⊥) :

function.injective t

theorem complete_lattice.independent_pair {α : Type u_1} {ι : Type u_3} [complete_lattice α] {t : ι → α} {i j : ι} (hij : i ≠ j) (huniv : ∀ (k : ι), k = i ∨ k = j) :

complete_lattice.independent t ↔ disjoint (t i) (t j)

theorem complete_lattice.independent.map_order_iso {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : α ≃o β) {a : ι → α} (ha : complete_lattice.independent a) :

complete_lattice.independent (⇑f ∘ a)

Composing an indepedent indexed family with an order isomorphism on the elements results in another indepedendent indexed family.

@[simp]

theorem complete_lattice.independent_map_order_iso_iff {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : α ≃o β) {a : ι → α} :

complete_lattice.independent (⇑f ∘ a) ↔ complete_lattice.independent a

theorem complete_lattice.independent.disjoint_bsupr {ι : Type u_1} {α : Type u_2} [complete_lattice α] {t : ι → α} (ht : complete_lattice.independent t) {x : ι} {y : set ι} (hx : x ∉ y) :

disjoint (t x) (⨆ (i : ι) (H : i ∈ y), t i)

If the elements of a set are independent, then any element is disjoint from the supr of some subset of the rest.

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

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 the forward direction of complete_lattice.independent_iff_sup_indep.

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 the reverse direction of complete_lattice.independent_iff_sup_indep.

theorem complete_lattice.independent_iff_sup_indep_univ {α : Type u_1} {ι : Type u_3} [complete_lattice α] [fintype ι] {f : ι → α} :

complete_lattice.independent f ↔ finset.univ.sup_indep f

A variant of complete_lattice.independent_iff_sup_indep for fintypes.

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

finset.univ.sup_indep f → complete_lattice.independent f

Alias of the reverse direction of complete_lattice.independent_iff_sup_indep_univ.

theorem complete_lattice.independent.sup_indep_univ {α : Type u_1} {ι : Type u_3} [complete_lattice α] [fintype ι] {f : ι → α} :

complete_lattice.independent f → finset.univ.sup_indep f

Alias of the forward direction of complete_lattice.independent_iff_sup_indep_univ.

theorem complete_lattice.set_independent_iff_pairwise_disjoint {α : Type u_1} [order.frame α] {s : set α} :

complete_lattice.set_independent s ↔ s.pairwise_disjoint id

theorem set.pairwise_disjoint.set_independent {α : Type u_1} [order.frame α] {s : set α} :

s.pairwise_disjoint id → complete_lattice.set_independent s

Alias of the reverse direction of complete_lattice.set_independent_iff_pairwise_disjoint.

theorem complete_lattice.independent_iff_pairwise_disjoint {α : Type u_1} {ι : Type u_3} [order.frame α] {f : ι → α} :

complete_lattice.independent f ↔ pairwise (disjoint on f)