# 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 #

• SupClosed: Predicate for a set to be closed under join (a ∈ s and b ∈ s imply a ⊔ b ∈ s).
• InfClosed: Predicate for a set to be closed under meet (a ∈ s and b ∈ s imply a ⊓ b ∈ s).
• supClosure: Sup-closure. Smallest sup-closed set containing a given set.
• infClosure: Inf-closure. Smallest inf-closed set containing a given set.
• SemilatticeSup.toCompleteSemilatticeSup: A join-semilattice where every sup-closed set has a least upper bound is automatically complete.
• SemilatticeInf.toCompleteSemilatticeInf: A meet-semilattice where every inf-closed set has a greatest lower bound is automatically complete.
def SupClosed {α : Type u_1} [] (s : Set α) :

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

Instances For
@[simp]
theorem supClosed_empty {α : Type u_1} [] :
@[simp]
theorem supClosed_singleton {α : Type u_1} [] {a : α} :
@[simp]
theorem supClosed_univ {α : Type u_1} [] :
SupClosed Set.univ
theorem SupClosed.inter {α : Type u_1} [] {s : Set α} {t : Set α} (hs : ) (ht : ) :
theorem supClosed_sInter {α : Type u_1} [] {S : Set (Set α)} (hS : ∀ (s : Set α), s S) :
theorem supClosed_iInter {α : Type u_1} [] {ι : Sort u_2} {f : ιSet α} (hf : ∀ (i : ι), SupClosed (f i)) :
SupClosed (⋂ (i : ι), f i)
theorem SupClosed.directedOn {α : Type u_1} [] {s : Set α} (hs : ) :
DirectedOn (fun x x_1 => x x_1) s
theorem SupClosed.finsetSup'_mem {α : Type u_1} [] {ι : Type u_2} {f : ια} {s : Set α} {t : } (hs : ) (ht : ) :
(∀ (i : ι), i tf i s) → Finset.sup' t ht f s
theorem SupClosed.finsetSup_mem {α : Type u_1} [] {ι : Type u_2} {f : ια} {s : Set α} {t : } [] (hs : ) (ht : ) :
(∀ (i : ι), i tf i s) → s
def InfClosed {α : Type u_1} [] (s : Set α) :

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

Instances For
@[simp]
theorem infClosed_empty {α : Type u_1} [] :
@[simp]
theorem infClosed_singleton {α : Type u_1} [] {a : α} :
@[simp]
theorem infClosed_univ {α : Type u_1} [] :
InfClosed Set.univ
theorem InfClosed.inter {α : Type u_1} [] {s : Set α} {t : Set α} (hs : ) (ht : ) :
theorem infClosed_sInter {α : Type u_1} [] {S : Set (Set α)} (hS : ∀ (s : Set α), s S) :
theorem infClosed_iInter {α : Type u_1} [] {ι : Sort u_2} {f : ιSet α} (hf : ∀ (i : ι), InfClosed (f i)) :
InfClosed (⋂ (i : ι), f i)
theorem InfClosed.codirectedOn {α : Type u_1} [] {s : Set α} (hs : ) :
DirectedOn (fun x x_1 => x x_1) s
theorem InfClosed.finsetInf'_mem {α : Type u_1} [] {ι : Type u_2} {f : ια} {s : Set α} {t : } (hs : ) (ht : ) :
(∀ (i : ι), i tf i s) → Finset.inf' t ht f s
theorem InfClosed.finsetInf_mem {α : Type u_1} [] {ι : Type u_2} {f : ια} {s : Set α} {t : } [] (hs : ) (ht : ) :
(∀ (i : ι), i tf i s) → s
@[simp]
theorem supClosed_preimage_toDual {α : Type u_1} [] {s : } :
SupClosed (OrderDual.toDual ⁻¹' s)
@[simp]
theorem infClosed_preimage_toDual {α : Type u_1} [] {s : } :
InfClosed (OrderDual.toDual ⁻¹' s)
@[simp]
theorem supClosed_preimage_ofDual {α : Type u_1} [] {s : Set α} :
SupClosed (OrderDual.ofDual ⁻¹' s)
@[simp]
theorem infClosed_preimage_ofDual {α : Type u_1} [] {s : Set α} :
InfClosed (OrderDual.ofDual ⁻¹' s)
theorem InfClosed.dual {α : Type u_1} [] {s : Set α} :
SupClosed (OrderDual.ofDual ⁻¹' s)

Alias of the reverse direction of supClosed_preimage_ofDual.

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

Alias of the reverse direction of infClosed_preimage_ofDual.

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

## Closure #

def supClosure {α : Type u_1} [] :

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

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

Alias of the reverse direction of supClosure_eq_self.

theorem supClosure_idem {α : Type u_1} [] (s : Set α) :
supClosure (supClosure s) = supClosure s
@[simp]
theorem supClosure_empty {α : Type u_1} [] :
supClosure =
@[simp]
theorem supClosure_singleton {α : Type u_1} [] {a : α} :
supClosure {a} = {a}
@[simp]
theorem supClosure_univ {α : Type u_1} [] :
supClosure Set.univ = Set.univ
@[simp]
theorem upperBounds_supClosure {α : Type u_1} [] (s : Set α) :
upperBounds (supClosure s) =
@[simp]
theorem isLUB_supClosure {α : Type u_1} [] {s : Set α} {a : α} :
IsLUB (supClosure s) a IsLUB s a
def infClosure {α : Type u_1} [] :

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

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

Alias of the reverse direction of infClosure_eq_self.

theorem infClosure_idem {α : Type u_1} [] (s : Set α) :
infClosure (infClosure s) = infClosure s
@[simp]
theorem infClosure_empty {α : Type u_1} [] :
infClosure =
@[simp]
theorem infClosure_singleton {α : Type u_1} [] {a : α} :
infClosure {a} = {a}
@[simp]
theorem infClosure_univ {α : Type u_1} [] :
infClosure Set.univ = Set.univ
@[simp]
theorem lowerBounds_infClosure {α : Type u_1} [] (s : Set α) :
lowerBounds (infClosure s) =
@[simp]
theorem isGLB_infClosure {α : Type u_1} [] {s : Set α} {a : α} :
IsGLB (infClosure s) a IsGLB s a
def SemilatticeSup.toCompleteSemilatticeSup {α : Type u_1} [] (sSup : Set αα) (h : ∀ (s : Set α), IsLUB s (sSup s)) :

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

Instances For
def SemilatticeInf.toCompleteSemilatticeInf {α : Type u_1} [] (sInf : Set αα) (h : ∀ (s : Set α), IsGLB s (sInf s)) :

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

Instances For