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
@[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
@[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.

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
@[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
@[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
@[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
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