Documentation

Mathlib.Order.SupIndep

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.

Main definitions #

Main statements #

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.SupIndep {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] (s : Finset ι) (f : ια) :

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

Equations
Instances For
    instance Finset.instDecidableSupIndep {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {f : ια} [DecidableEq ι] [DecidableEq α] :
    Equations
    • Finset.instDecidableSupIndep = Finset.decidableForallOfDecidableSubsets
    theorem Finset.SupIndep.subset {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {t : Finset ι} {f : ια} (ht : Finset.SupIndep t f) (h : s t) :
    @[simp]
    theorem Finset.supIndep_empty {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] (f : ια) :
    theorem Finset.supIndep_singleton {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] (i : ι) (f : ια) :
    theorem Finset.SupIndep.pairwiseDisjoint {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {f : ια} (hs : Finset.SupIndep s f) :
    theorem Finset.SupIndep.le_sup_iff {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {t : Finset ι} {f : ια} {i : ι} (hs : Finset.SupIndep s f) (hts : t s) (hi : i s) (hf : ∀ (i : ι), f i ) :
    f i Finset.sup t f i t
    theorem Finset.supIndep_iff_disjoint_erase {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {f : ια} [DecidableEq ι] :
    Finset.SupIndep s f is, Disjoint (f i) (Finset.sup (Finset.erase s i) f)

    The RHS looks like the definition of CompleteLattice.Independent.

    theorem Finset.SupIndep.image {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [Lattice α] [OrderBot α] {f : ια} [DecidableEq ι] {s : Finset ι'} {g : ι'ι} (hs : Finset.SupIndep s (f g)) :
    theorem Finset.supIndep_map {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [Lattice α] [OrderBot α] {f : ια} {s : Finset ι'} {g : ι' ι} :
    @[simp]
    theorem Finset.supIndep_pair {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {f : ια} [DecidableEq ι] {i : ι} {j : ι} (hij : i j) :
    Finset.SupIndep {i, j} f Disjoint (f i) (f j)
    theorem Finset.supIndep_univ_bool {α : Type u_1} [Lattice α] [OrderBot α] (f : Boolα) :
    Finset.SupIndep Finset.univ f Disjoint (f false) (f true)
    @[simp]
    theorem Finset.supIndep_univ_fin_two {α : Type u_1} [Lattice α] [OrderBot α] (f : Fin 2α) :
    Finset.SupIndep Finset.univ f Disjoint (f 0) (f 1)
    theorem Finset.SupIndep.attach {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {f : ια} (hs : Finset.SupIndep s f) :
    Finset.SupIndep (Finset.attach s) fun (a : { x : ι // x s }) => f a
    @[simp]
    theorem Finset.supIndep_attach {α : Type u_1} {ι : Type u_3} [Lattice α] [OrderBot α] {s : Finset ι} {f : ια} :
    (Finset.SupIndep (Finset.attach s) fun (a : { x : ι // x s }) => f a) Finset.SupIndep s f
    theorem Finset.supIndep_iff_pairwiseDisjoint {α : Type u_1} {ι : Type u_3} [DistribLattice α] [OrderBot α] {s : Finset ι} {f : ια} :
    theorem Finset.sup_indep.pairwise_disjoint {α : Type u_1} {ι : Type u_3} [DistribLattice α] [OrderBot α] {s : Finset ι} {f : ια} :

    Alias of the forward direction of Finset.supIndep_iff_pairwiseDisjoint.

    theorem Set.PairwiseDisjoint.supIndep {α : Type u_1} {ι : Type u_3} [DistribLattice α] [OrderBot α] {s : Finset ι} {f : ια} :

    Alias of the reverse direction of Finset.supIndep_iff_pairwiseDisjoint.

    theorem Finset.SupIndep.sup {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [DistribLattice α] [OrderBot α] [DecidableEq ι] {s : Finset ι'} {g : ι'Finset ι} {f : ια} (hs : Finset.SupIndep s fun (i : ι') => Finset.sup (g i) f) (hg : i's, Finset.SupIndep (g i') f) :

    Bind operation for SupIndep.

    theorem Finset.SupIndep.biUnion {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [DistribLattice α] [OrderBot α] [DecidableEq ι] {s : Finset ι'} {g : ι'Finset ι} {f : ια} (hs : Finset.SupIndep s fun (i : ι') => Finset.sup (g i) f) (hg : i's, Finset.SupIndep (g i') f) :

    Bind operation for SupIndep.

    theorem Finset.SupIndep.sigma {α : Type u_1} {ι : Type u_3} [DistribLattice α] [OrderBot α] {β : ιType u_5} {s : Finset ι} {g : (i : ι) → Finset (β i)} {f : Sigma βα} (hs : Finset.SupIndep s fun (i : ι) => Finset.sup (g i) fun (b : β i) => f { fst := i, snd := b }) (hg : is, Finset.SupIndep (g i) fun (b : β i) => f { fst := i, snd := b }) :

    Bind operation for SupIndep.

    theorem Finset.SupIndep.product {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [DistribLattice α] [OrderBot α] {s : Finset ι} {t : Finset ι'} {f : ι × ι'α} (hs : Finset.SupIndep s fun (i : ι) => Finset.sup t fun (i' : ι') => f (i, i')) (ht : Finset.SupIndep t fun (i' : ι') => Finset.sup s fun (i : ι) => f (i, i')) :
    theorem Finset.supIndep_product_iff {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} [DistribLattice α] [OrderBot α] {s : Finset ι} {t : Finset ι'} {f : ι × ι'α} :
    Finset.SupIndep (Finset.product s t) f (Finset.SupIndep s fun (i : ι) => Finset.sup t fun (i' : ι') => f (i, i')) Finset.SupIndep t fun (i' : ι') => Finset.sup s fun (i : ι) => f (i, i')

    On complete lattices via sSup #

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

    Equations
    Instances For

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

      theorem CompleteLattice.setIndependent_pair {α : Type u_1} [CompleteLattice α] {a : α} {b : α} (hab : a b) :
      theorem CompleteLattice.SetIndependent.disjoint_sSup {α : Type u_1} [CompleteLattice α] {s : Set α} (hs : CompleteLattice.SetIndependent s) {x : α} {y : Set α} (hx : x s) (hy : y s) (hxy : xy) :

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

      def CompleteLattice.Independent {ι : Sort u_5} {α : Type u_6} [CompleteLattice α] (t : ια) :

      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.

      Equations
      Instances For
        theorem CompleteLattice.independent_def {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ια} :
        CompleteLattice.Independent t ∀ (i : ι), Disjoint (t i) (⨆ (j : ι), ⨆ (_ : j i), t j)
        theorem CompleteLattice.independent_def' {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ια} :
        CompleteLattice.Independent t ∀ (i : ι), Disjoint (t i) (sSup (t '' {j : ι | j i}))
        theorem CompleteLattice.independent_def'' {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ια} :
        CompleteLattice.Independent t ∀ (i : ι), Disjoint (t i) (sSup {a : α | ∃ (j : ι), j i t j = a})
        theorem CompleteLattice.Independent.pairwiseDisjoint {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ια} (ht : CompleteLattice.Independent t) :
        Pairwise (Disjoint on t)

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

        theorem CompleteLattice.Independent.mono {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {s : ια} {t : ια} (hs : CompleteLattice.Independent s) (hst : t s) :
        theorem CompleteLattice.Independent.comp {α : Type u_1} [CompleteLattice α] {ι : Sort u_5} {ι' : Sort u_6} {t : ια} {f : ι'ι} (ht : CompleteLattice.Independent t) (hf : Function.Injective f) :

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

        theorem CompleteLattice.Independent.comp' {α : Type u_1} [CompleteLattice α] {ι : Sort u_5} {ι' : Sort u_6} {t : ια} {f : ι'ι} (ht : CompleteLattice.Independent (t f)) (hf : Function.Surjective f) :
        @[simp]
        theorem CompleteLattice.independent_ne_bot_iff_independent {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ια} :
        (CompleteLattice.Independent fun (i : { i : ι // t i }) => t i) CompleteLattice.Independent t
        theorem CompleteLattice.Independent.injOn {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ια} (ht : CompleteLattice.Independent t) :
        Set.InjOn t {i : ι | t i }
        theorem CompleteLattice.Independent.injective {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ια} (ht : CompleteLattice.Independent t) (h_ne_bot : ∀ (i : ι), t i ) :
        theorem CompleteLattice.independent_pair {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ια} {i : ι} {j : ι} (hij : i j) (huniv : ∀ (k : ι), k = i k = j) :
        theorem CompleteLattice.Independent.map_orderIso {ι : Sort u_5} {α : Type u_6} {β : Type u_7} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) {a : ια} (ha : CompleteLattice.Independent a) :

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

        @[simp]
        theorem CompleteLattice.independent_map_orderIso_iff {ι : Sort u_5} {α : Type u_6} {β : Type u_7} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) {a : ια} :
        theorem CompleteLattice.Independent.disjoint_biSup {ι : Type u_5} {α : Type u_6} [CompleteLattice α] {t : ια} (ht : CompleteLattice.Independent t) {x : ι} {y : Set ι} (hx : xy) :
        Disjoint (t x) (⨆ i ∈ y, t i)

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

        theorem CompleteLattice.independent_iff_supIndep {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {s : Finset ι} {f : ια} :
        theorem CompleteLattice.Independent.supIndep {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {s : Finset ι} {f : ια} :

        Alias of the forward direction of CompleteLattice.independent_iff_supIndep.

        theorem Finset.SupIndep.independent {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {s : Finset ι} {f : ια} :

        Alias of the reverse direction of CompleteLattice.independent_iff_supIndep.

        theorem CompleteLattice.Independent.supIndep' {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {f : ια} (s : Finset ι) (h : CompleteLattice.Independent f) :
        theorem Finset.SupIndep.independent_of_univ {α : Type u_1} {ι : Type u_3} [CompleteLattice α] [Fintype ι] {f : ια} :

        Alias of the reverse direction of CompleteLattice.independent_iff_supIndep_univ.


        A variant of CompleteLattice.independent_iff_supIndep for Fintypes.