# 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).
• IsSublattice: Predicate for a set to be closed under meet and join.
• supClosure: Sup-closure. Smallest sup-closed set containing a given set.
• infClosure: Inf-closure. Smallest inf-closed set containing a given set.
• latticeClosure: Smallest sublattice 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_2} [] (s : Set α) :

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

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

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

Equations
• = ∀ ⦃a : α⦄, a s∀ ⦃b : α⦄, b sa b s
Instances For
@[simp]
theorem infClosed_empty {α : Type u_2} [] :
@[simp]
theorem infClosed_singleton {α : Type u_2} [] {a : α} :
@[simp]
theorem infClosed_univ {α : Type u_2} [] :
InfClosed Set.univ
theorem InfClosed.inter {α : Type u_2} [] {s : Set α} {t : Set α} (hs : ) (ht : ) :
theorem infClosed_sInter {α : Type u_2} [] {S : Set (Set α)} (hS : sS, ) :
theorem infClosed_iInter {α : Type u_2} [] {ι : Sort u_4} {f : ιSet α} (hf : ∀ (i : ι), InfClosed (f i)) :
InfClosed (⋂ (i : ι), f i)
theorem InfClosed.codirectedOn {α : Type u_2} [] {s : Set α} (hs : ) :
DirectedOn (fun (x x_1 : α) => x x_1) s
theorem IsLowerSet.infClosed {α : Type u_2} [] {s : Set α} (hs : ) :
theorem InfClosed.preimage {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set α} [FunLike F β α] [InfHomClass F β α] (hs : ) (f : F) :
InfClosed (f ⁻¹' s)
theorem InfClosed.image {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set α} [FunLike F α β] [InfHomClass F α β] (hs : ) (f : F) :
InfClosed (f '' s)
theorem infClosed_range {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [InfHomClass F α β] (f : F) :
theorem InfClosed.prod {α : Type u_2} {β : Type u_3} [] [] {s : Set α} {t : Set β} (hs : ) (ht : ) :
theorem infClosed_pi {ι : Type u_5} {α : ιType u_6} [(i : ι) → SemilatticeInf (α i)] {s : Set ι} {t : (i : ι) → Set (α i)} (ht : is, InfClosed (t i)) :
theorem InfClosed.finsetInf'_mem {α : Type u_2} [] {ι : Type u_4} {f : ια} {s : Set α} {t : } (hs : ) (ht : t.Nonempty) :
(it, f i s)Finset.inf' t ht f s
theorem InfClosed.finsetInf_mem {α : Type u_2} [] {ι : Type u_4} {f : ια} {s : Set α} {t : } [] (hs : ) (ht : t.Nonempty) :
(it, f i s) s
structure IsSublattice {α : Type u_2} [] (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.

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

Alias of the reverse direction of supClosed_preimage_ofDual.

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

Alias of the reverse direction of infClosed_preimage_ofDual.

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

Alias of the reverse direction of isSublattice_preimage_ofDual.

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

Alias of the reverse direction of isSublattice_preimage_toDual.

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

## Closure #

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

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

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

Alias of the reverse direction of supClosure_eq_self.

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

The semilatice generated by a finite set is finite.

@[simp]
theorem infClosure_isClosed {α : Type u_2} [] (s : Set α) :
infClosure.IsClosed s =
def infClosure {α : Type u_2} [] :

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

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

Alias of the reverse direction of infClosure_eq_self.

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

The semilatice generated by a finite set is finite.

@[simp]
theorem latticeClosure_isClosed {α : Type u_2} [] (s : Set α) :
latticeClosure.IsClosed s =
def latticeClosure {α : Type u_2} [] :

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

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

Alias of the reverse direction of latticeClosure_eq_self.

theorem latticeClosure_idem {α : Type u_2} [] (s : Set α) :
latticeClosure (latticeClosure s) = latticeClosure s
@[simp]
theorem latticeClosure_empty {α : Type u_2} [] :
latticeClosure =
@[simp]
theorem latticeClosure_singleton {α : Type u_2} [] (a : α) :
latticeClosure {a} = {a}
@[simp]
theorem latticeClosure_univ {α : Type u_2} [] :
latticeClosure Set.univ = Set.univ
theorem SupClosed.infClosure {α : Type u_2} [] {s : Set α} (hs : ) :
SupClosed (infClosure s)
theorem InfClosed.supClosure {α : Type u_2} [] {s : Set α} (hs : ) :
InfClosed (supClosure s)
@[simp]
theorem supClosure_infClosure {α : Type u_2} [] (s : Set α) :
supClosure (infClosure s) = latticeClosure s
@[simp]
theorem infClosure_supClosure {α : Type u_2} [] (s : Set α) :
infClosure (supClosure s) = latticeClosure s
theorem Set.Finite.latticeClosure {α : Type u_2} [] {s : Set α} (hs : ) :
Set.Finite (latticeClosure s)
def SemilatticeSup.toCompleteSemilatticeSup {α : Type u_2} [] (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.

Equations
Instances For
def SemilatticeInf.toCompleteSemilatticeInf {α : Type u_2} [] (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.

Equations
Instances For