Documentation

Mathlib.Order.SupClosed

Sets closed under join/meet #

This file defines predicates for sets closed under and shows that each set in a join-semilattice generates a join-closed set and that a semilattice where every directed set has a least upper bound is automatically complete. All dually for .

Main declarations #

def SupClosed {α : Type u_2} [SemilatticeSup α] (s : Set α) :

A set s is sup-closed if a ⊔ b ∈ s for all a ∈ s, b ∈ s.

Equations
Instances For
    @[simp]
    @[simp]
    theorem supClosed_singleton {α : Type u_2} [SemilatticeSup α] {a : α} :
    @[simp]
    theorem supClosed_univ {α : Type u_2} [SemilatticeSup α] :
    SupClosed Set.univ
    theorem SupClosed.inter {α : Type u_2} [SemilatticeSup α] {s : Set α} {t : Set α} (hs : SupClosed s) (ht : SupClosed t) :
    theorem supClosed_sInter {α : Type u_2} [SemilatticeSup α] {S : Set (Set α)} (hS : sS, SupClosed s) :
    theorem supClosed_iInter {α : Type u_2} [SemilatticeSup α] {ι : Sort u_4} {f : ιSet α} (hf : ∀ (i : ι), SupClosed (f i)) :
    SupClosed (⋂ (i : ι), f i)
    theorem SupClosed.directedOn {α : Type u_2} [SemilatticeSup α] {s : Set α} (hs : SupClosed s) :
    DirectedOn (fun (x1 x2 : α) => x1 x2) s
    theorem IsUpperSet.supClosed {α : Type u_2} [SemilatticeSup α] {s : Set α} (hs : IsUpperSet s) :
    theorem SupClosed.preimage {F : Type u_1} {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [SemilatticeSup β] {s : Set α} [FunLike F β α] [SupHomClass F β α] (hs : SupClosed s) (f : F) :
    SupClosed (f ⁻¹' s)
    theorem SupClosed.image {F : Type u_1} {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [SemilatticeSup β] {s : Set α} [FunLike F α β] [SupHomClass F α β] (hs : SupClosed s) (f : F) :
    SupClosed (f '' s)
    theorem supClosed_range {F : Type u_1} {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [SemilatticeSup β] [FunLike F α β] [SupHomClass F α β] (f : F) :
    theorem SupClosed.prod {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [SemilatticeSup β] {s : Set α} {t : Set β} (hs : SupClosed s) (ht : SupClosed t) :
    theorem supClosed_pi {ι : Type u_5} {α : ιType u_6} [(i : ι) → SemilatticeSup (α i)] {s : Set ι} {t : (i : ι) → Set (α i)} (ht : is, SupClosed (t i)) :
    SupClosed (s.pi t)
    theorem SupClosed.finsetSup'_mem {α : Type u_2} [SemilatticeSup α] {ι : Type u_4} {f : ια} {s : Set α} {t : Finset ι} (hs : SupClosed s) (ht : t.Nonempty) :
    (∀ it, f i s)t.sup' ht f s
    theorem SupClosed.finsetSup_mem {α : Type u_2} [SemilatticeSup α] {ι : Type u_4} {f : ια} {s : Set α} {t : Finset ι} [OrderBot α] (hs : SupClosed s) (ht : t.Nonempty) :
    (∀ it, f i s)t.sup f s
    def InfClosed {α : Type u_2} [SemilatticeInf α] (s : Set α) :

    A set s is inf-closed if a ⊓ b ∈ s for all a ∈ s, b ∈ s.

    Equations
    Instances For
      @[simp]
      @[simp]
      theorem infClosed_singleton {α : Type u_2} [SemilatticeInf α] {a : α} :
      @[simp]
      theorem infClosed_univ {α : Type u_2} [SemilatticeInf α] :
      InfClosed Set.univ
      theorem InfClosed.inter {α : Type u_2} [SemilatticeInf α] {s : Set α} {t : Set α} (hs : InfClosed s) (ht : InfClosed t) :
      theorem infClosed_sInter {α : Type u_2} [SemilatticeInf α] {S : Set (Set α)} (hS : sS, InfClosed s) :
      theorem infClosed_iInter {α : Type u_2} [SemilatticeInf α] {ι : Sort u_4} {f : ιSet α} (hf : ∀ (i : ι), InfClosed (f i)) :
      InfClosed (⋂ (i : ι), f i)
      theorem InfClosed.codirectedOn {α : Type u_2} [SemilatticeInf α] {s : Set α} (hs : InfClosed s) :
      DirectedOn (fun (x1 x2 : α) => x1 x2) s
      theorem IsLowerSet.infClosed {α : Type u_2} [SemilatticeInf α] {s : Set α} (hs : IsLowerSet s) :
      theorem InfClosed.preimage {F : Type u_1} {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [SemilatticeInf β] {s : Set α} [FunLike F β α] [InfHomClass F β α] (hs : InfClosed s) (f : F) :
      InfClosed (f ⁻¹' s)
      theorem InfClosed.image {F : Type u_1} {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [SemilatticeInf β] {s : Set α} [FunLike F α β] [InfHomClass F α β] (hs : InfClosed s) (f : F) :
      InfClosed (f '' s)
      theorem infClosed_range {F : Type u_1} {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [SemilatticeInf β] [FunLike F α β] [InfHomClass F α β] (f : F) :
      theorem InfClosed.prod {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [SemilatticeInf β] {s : Set α} {t : Set β} (hs : InfClosed s) (ht : InfClosed t) :
      theorem infClosed_pi {ι : Type u_5} {α : ιType u_6} [(i : ι) → SemilatticeInf (α i)] {s : Set ι} {t : (i : ι) → Set (α i)} (ht : is, InfClosed (t i)) :
      InfClosed (s.pi t)
      theorem InfClosed.finsetInf'_mem {α : Type u_2} [SemilatticeInf α] {ι : Type u_4} {f : ια} {s : Set α} {t : Finset ι} (hs : InfClosed s) (ht : t.Nonempty) :
      (∀ it, f i s)t.inf' ht f s
      theorem InfClosed.finsetInf_mem {α : Type u_2} [SemilatticeInf α] {ι : Type u_4} {f : ια} {s : Set α} {t : Finset ι} [OrderTop α] (hs : InfClosed s) (ht : t.Nonempty) :
      (∀ it, f i s)t.inf f s
      structure IsSublattice {α : Type u_2} [Lattice α] (s : Set α) :

      A set s is a sublattice if a ⊔ b ∈ s and a ⊓ b ∈ s for all a ∈ s, b ∈ s. Note: This is not the preferred way to declare a sublattice. One should instead use Sublattice. TODO: Define Sublattice.

      Instances For
        theorem IsSublattice.supClosed {α : Type u_2} [Lattice α] {s : Set α} (self : IsSublattice s) :
        theorem IsSublattice.infClosed {α : Type u_2} [Lattice α] {s : Set α} (self : IsSublattice s) :
        @[simp]
        @[simp]
        theorem isSublattice_singleton {α : Type u_2} [Lattice α] {a : α} :
        @[simp]
        theorem isSublattice_univ {α : Type u_2} [Lattice α] :
        IsSublattice Set.univ
        theorem IsSublattice.inter {α : Type u_2} [Lattice α] {s : Set α} {t : Set α} (hs : IsSublattice s) (ht : IsSublattice t) :
        theorem isSublattice_sInter {α : Type u_2} [Lattice α] {S : Set (Set α)} (hS : sS, IsSublattice s) :
        theorem isSublattice_iInter {α : Type u_2} {ι : Sort u_4} [Lattice α] {f : ιSet α} (hf : ∀ (i : ι), IsSublattice (f i)) :
        IsSublattice (⋂ (i : ι), f i)
        theorem IsSublattice.preimage {F : Type u_1} {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {s : Set α} [FunLike F β α] [LatticeHomClass F β α] (hs : IsSublattice s) (f : F) :
        theorem IsSublattice.image {F : Type u_1} {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {s : Set α} [FunLike F α β] [LatticeHomClass F α β] (hs : IsSublattice s) (f : F) :
        IsSublattice (f '' s)
        theorem IsSublattice_range {F : Type u_1} {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [FunLike F α β] [LatticeHomClass F α β] (f : F) :
        theorem IsSublattice.prod {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {s : Set α} {t : Set β} (hs : IsSublattice s) (ht : IsSublattice t) :
        theorem isSublattice_pi {ι : Type u_5} {α : ιType u_6} [(i : ι) → Lattice (α i)] {s : Set ι} {t : (i : ι) → Set (α i)} (ht : is, IsSublattice (t i)) :
        IsSublattice (s.pi t)
        @[simp]
        theorem supClosed_preimage_toDual {α : Type u_2} [Lattice α] {s : Set αᵒᵈ} :
        SupClosed (OrderDual.toDual ⁻¹' s) InfClosed s
        @[simp]
        theorem infClosed_preimage_toDual {α : Type u_2} [Lattice α] {s : Set αᵒᵈ} :
        InfClosed (OrderDual.toDual ⁻¹' s) SupClosed s
        @[simp]
        theorem supClosed_preimage_ofDual {α : Type u_2} [Lattice α] {s : Set α} :
        SupClosed (OrderDual.ofDual ⁻¹' s) InfClosed s
        @[simp]
        theorem infClosed_preimage_ofDual {α : Type u_2} [Lattice α] {s : Set α} :
        InfClosed (OrderDual.ofDual ⁻¹' s) SupClosed s
        @[simp]
        theorem isSublattice_preimage_toDual {α : Type u_2} [Lattice α] {s : Set αᵒᵈ} :
        IsSublattice (OrderDual.toDual ⁻¹' s) IsSublattice s
        @[simp]
        theorem isSublattice_preimage_ofDual {α : Type u_2} [Lattice α] {s : Set α} :
        IsSublattice (OrderDual.ofDual ⁻¹' s) IsSublattice s
        theorem InfClosed.dual {α : Type u_2} [Lattice α] {s : Set α} :
        InfClosed sSupClosed (OrderDual.ofDual ⁻¹' s)

        Alias of the reverse direction of supClosed_preimage_ofDual.

        theorem SupClosed.dual {α : Type u_2} [Lattice α] {s : Set α} :
        SupClosed sInfClosed (OrderDual.ofDual ⁻¹' s)

        Alias of the reverse direction of infClosed_preimage_ofDual.

        theorem IsSublattice.dual {α : Type u_2} [Lattice α] {s : Set α} :
        IsSublattice sIsSublattice (OrderDual.ofDual ⁻¹' s)

        Alias of the reverse direction of isSublattice_preimage_ofDual.

        theorem IsSublattice.of_dual {α : Type u_2} [Lattice α] {s : Set αᵒᵈ} :
        IsSublattice sIsSublattice (OrderDual.toDual ⁻¹' s)

        Alias of the reverse direction of isSublattice_preimage_toDual.

        @[simp]
        theorem LinearOrder.supClosed {α : Type u_2} [LinearOrder α] (s : Set α) :
        @[simp]
        theorem LinearOrder.infClosed {α : Type u_2} [LinearOrder α] (s : Set α) :
        @[simp]
        theorem LinearOrder.isSublattice {α : Type u_2} [LinearOrder α] (s : Set α) :

        Closure #

        @[simp]
        theorem supClosure_isClosed {α : Type u_2} [SemilatticeSup α] (s : Set α) :
        supClosure.IsClosed s = SupClosed s

        Every set in a join-semilattice generates a set closed under join.

        Equations
        Instances For
          @[simp]
          theorem subset_supClosure {α : Type u_2} [SemilatticeSup α] {s : Set α} :
          s supClosure s
          @[simp]
          theorem supClosed_supClosure {α : Type u_2} [SemilatticeSup α] {s : Set α} :
          SupClosed (supClosure s)
          theorem supClosure_mono {α : Type u_2} [SemilatticeSup α] :
          Monotone supClosure
          @[simp]
          theorem supClosure_eq_self {α : Type u_2} [SemilatticeSup α] {s : Set α} :
          supClosure s = s SupClosed s
          theorem SupClosed.supClosure_eq {α : Type u_2} [SemilatticeSup α] {s : Set α} :
          SupClosed ssupClosure s = s

          Alias of the reverse direction of supClosure_eq_self.

          theorem supClosure_idem {α : Type u_2} [SemilatticeSup α] (s : Set α) :
          supClosure (supClosure s) = supClosure s
          @[simp]
          theorem supClosure_empty {α : Type u_2} [SemilatticeSup α] :
          supClosure =
          @[simp]
          theorem supClosure_singleton {α : Type u_2} [SemilatticeSup α] {a : α} :
          supClosure {a} = {a}
          @[simp]
          theorem supClosure_univ {α : Type u_2} [SemilatticeSup α] :
          supClosure Set.univ = Set.univ
          @[simp]
          theorem upperBounds_supClosure {α : Type u_2} [SemilatticeSup α] (s : Set α) :
          upperBounds (supClosure s) = upperBounds s
          @[simp]
          theorem isLUB_supClosure {α : Type u_2} [SemilatticeSup α] {s : Set α} {a : α} :
          IsLUB (supClosure s) a IsLUB s a
          theorem sup_mem_supClosure {α : Type u_2} [SemilatticeSup α] {s : Set α} {a : α} {b : α} (ha : a s) (hb : b s) :
          a b supClosure s
          theorem finsetSup'_mem_supClosure {α : Type u_2} [SemilatticeSup α] {s : Set α} {ι : Type u_4} {t : Finset ι} (ht : t.Nonempty) {f : ια} (hf : it, f i s) :
          t.sup' ht f supClosure s
          theorem supClosure_min {α : Type u_2} [SemilatticeSup α] {s : Set α} {t : Set α} :
          s tSupClosed tsupClosure s t
          theorem Set.Finite.supClosure {α : Type u_2} [SemilatticeSup α] {s : Set α} (hs : s.Finite) :
          (supClosure s).Finite

          The semilatice generated by a finite set is finite.

          @[simp]
          theorem supClosure_prod {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [SemilatticeSup β] (s : Set α) (t : Set β) :
          supClosure (s ×ˢ t) = supClosure s ×ˢ supClosure t
          @[simp]
          theorem infClosure_isClosed {α : Type u_2} [SemilatticeInf α] (s : Set α) :
          infClosure.IsClosed s = InfClosed s

          Every set in a join-semilattice generates a set closed under join.

          Equations
          Instances For
            @[simp]
            theorem subset_infClosure {α : Type u_2} [SemilatticeInf α] {s : Set α} :
            s infClosure s
            @[simp]
            theorem infClosed_infClosure {α : Type u_2} [SemilatticeInf α] {s : Set α} :
            InfClosed (infClosure s)
            theorem infClosure_mono {α : Type u_2} [SemilatticeInf α] :
            Monotone infClosure
            @[simp]
            theorem infClosure_eq_self {α : Type u_2} [SemilatticeInf α] {s : Set α} :
            infClosure s = s InfClosed s
            theorem InfClosed.infClosure_eq {α : Type u_2} [SemilatticeInf α] {s : Set α} :
            InfClosed sinfClosure s = s

            Alias of the reverse direction of infClosure_eq_self.

            theorem infClosure_idem {α : Type u_2} [SemilatticeInf α] (s : Set α) :
            infClosure (infClosure s) = infClosure s
            @[simp]
            theorem infClosure_empty {α : Type u_2} [SemilatticeInf α] :
            infClosure =
            @[simp]
            theorem infClosure_singleton {α : Type u_2} [SemilatticeInf α] {a : α} :
            infClosure {a} = {a}
            @[simp]
            theorem infClosure_univ {α : Type u_2} [SemilatticeInf α] :
            infClosure Set.univ = Set.univ
            @[simp]
            theorem lowerBounds_infClosure {α : Type u_2} [SemilatticeInf α] (s : Set α) :
            lowerBounds (infClosure s) = lowerBounds s
            @[simp]
            theorem isGLB_infClosure {α : Type u_2} [SemilatticeInf α] {s : Set α} {a : α} :
            IsGLB (infClosure s) a IsGLB s a
            theorem inf_mem_infClosure {α : Type u_2} [SemilatticeInf α] {s : Set α} {a : α} {b : α} (ha : a s) (hb : b s) :
            a b infClosure s
            theorem finsetInf'_mem_infClosure {α : Type u_2} [SemilatticeInf α] {s : Set α} {ι : Type u_4} {t : Finset ι} (ht : t.Nonempty) {f : ια} (hf : it, f i s) :
            t.inf' ht f infClosure s
            theorem infClosure_min {α : Type u_2} [SemilatticeInf α] {s : Set α} {t : Set α} :
            s tInfClosed tinfClosure s t
            theorem Set.Finite.infClosure {α : Type u_2} [SemilatticeInf α] {s : Set α} (hs : s.Finite) :
            (infClosure s).Finite

            The semilatice generated by a finite set is finite.

            @[simp]
            theorem infClosure_prod {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [SemilatticeInf β] (s : Set α) (t : Set β) :
            infClosure (s ×ˢ t) = infClosure s ×ˢ infClosure t
            @[simp]
            theorem latticeClosure_isClosed {α : Type u_2} [Lattice α] (s : Set α) :
            latticeClosure.IsClosed s = IsSublattice s
            def latticeClosure {α : Type u_2} [Lattice α] :

            Every set in a join-semilattice generates a set closed under join.

            Equations
            Instances For
              @[simp]
              theorem subset_latticeClosure {α : Type u_2} [Lattice α] {s : Set α} :
              s latticeClosure s
              @[simp]
              theorem isSublattice_latticeClosure {α : Type u_2} [Lattice α] {s : Set α} :
              IsSublattice (latticeClosure s)
              theorem latticeClosure_min {α : Type u_2} [Lattice α] {s : Set α} {t : Set α} :
              s tIsSublattice tlatticeClosure s t
              theorem latticeClosure_mono {α : Type u_2} [Lattice α] :
              Monotone latticeClosure
              @[simp]
              theorem latticeClosure_eq_self {α : Type u_2} [Lattice α] {s : Set α} :
              latticeClosure s = s IsSublattice s
              theorem IsSublattice.latticeClosure_eq {α : Type u_2} [Lattice α] {s : Set α} :
              IsSublattice slatticeClosure s = s

              Alias of the reverse direction of latticeClosure_eq_self.

              theorem latticeClosure_idem {α : Type u_2} [Lattice α] (s : Set α) :
              latticeClosure (latticeClosure s) = latticeClosure s
              @[simp]
              theorem latticeClosure_empty {α : Type u_2} [Lattice α] :
              latticeClosure =
              @[simp]
              theorem latticeClosure_singleton {α : Type u_2} [Lattice α] (a : α) :
              latticeClosure {a} = {a}
              @[simp]
              theorem latticeClosure_univ {α : Type u_2} [Lattice α] :
              latticeClosure Set.univ = Set.univ
              theorem SupClosed.infClosure {α : Type u_2} [DistribLattice α] {s : Set α} (hs : SupClosed s) :
              SupClosed (infClosure s)
              theorem InfClosed.supClosure {α : Type u_2} [DistribLattice α] {s : Set α} (hs : InfClosed s) :
              InfClosed (supClosure s)
              @[simp]
              theorem supClosure_infClosure {α : Type u_2} [DistribLattice α] (s : Set α) :
              supClosure (infClosure s) = latticeClosure s
              @[simp]
              theorem infClosure_supClosure {α : Type u_2} [DistribLattice α] (s : Set α) :
              infClosure (supClosure s) = latticeClosure s
              theorem Set.Finite.latticeClosure {α : Type u_2} [DistribLattice α] {s : Set α} (hs : s.Finite) :
              (latticeClosure s).Finite
              @[simp]
              theorem latticeClosure_prod {α : Type u_2} {β : Type u_3} [DistribLattice α] [DistribLattice β] (s : Set α) (t : Set β) :
              latticeClosure (s ×ˢ t) = latticeClosure s ×ˢ latticeClosure t
              def SemilatticeSup.toCompleteSemilatticeSup {α : Type u_2} [SemilatticeSup α] (sSup : Set αα) (h : ∀ (s : Set α), SupClosed sIsLUB s (sSup s)) :

              A join-semilattice where every sup-closed set has a least upper bound is automatically complete.

              Equations
              Instances For
                def SemilatticeInf.toCompleteSemilatticeInf {α : Type u_2} [SemilatticeInf α] (sInf : Set αα) (h : ∀ (s : Set α), InfClosed sIsGLB s (sInf s)) :

                A meet-semilattice where every inf-closed set has a greatest lower bound is automatically complete.

                Equations
                Instances For