doc-next-gen

Mathlib.Order.SupClosed

Module docstring

{"# 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. ","## Closure "}
SupClosed definition
(s : Set α) : Prop
Full source 
/-- A set `s` is *sup-closed* if `a ⊔ b ∈ s` for all `a ∈ s`, `b ∈ s`. -/
def SupClosed (s : Set α) : Prop := ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → a ⊔ ba ⊔ b ∈ s
Sup-closed set
Informal description
A subset $s$ of a type $\alpha$ with a join operation $\sqcup$ is called *sup-closed* if for any two elements $a, b \in s$, their join $a \sqcup b$ is also in $s$.
supClosed_empty theorem
: SupClosed (∅ : Set α)
Full source 
@[simp] lemma supClosed_empty : SupClosed (∅ : Set α) := by simp [SupClosed]
Empty Set is Sup-Closed
Informal description
The empty set is sup-closed, i.e., for any type $\alpha$ with a join operation $\sqcup$, the empty set $\emptyset$ satisfies the condition that for any two elements $a, b \in \emptyset$, their join $a \sqcup b$ is also in $\emptyset$.
supClosed_singleton theorem
: SupClosed ({ a } : Set α)
Full source 
@[simp] lemma supClosed_singleton : SupClosed ({a} : Set α) := by simp [SupClosed]
Singleton Sets are Sup-Closed
Informal description
For any element $a$ of a type $\alpha$ with a join operation $\sqcup$, the singleton set $\{a\}$ is sup-closed.
supClosed_univ theorem
: SupClosed (univ : Set α)
Full source 
@[simp] lemma supClosed_univ : SupClosed (univ : Set α) := by simp [SupClosed]
Universal Set is Sup-Closed
Informal description
The universal set `univ` (the set of all elements of type `α`) is sup-closed, meaning that for any two elements $a, b \in \alpha$, their join $a \sqcup b$ is also in $\alpha$.
SupClosed.inter theorem
(hs : SupClosed s) (ht : SupClosed t) : SupClosed (s ∩ t)
Full source 
lemma SupClosed.inter (hs : SupClosed s) (ht : SupClosed t) : SupClosed (s ∩ t) :=
  fun _a ha _b hb ↦ ⟨hs ha.1 hb.1, ht ha.2 hb.2⟩
Intersection of Sup-Closed Sets is Sup-Closed
Informal description
If two subsets $s$ and $t$ of a type $\alpha$ with a join operation $\sqcup$ are both sup-closed, then their intersection $s \cap t$ is also sup-closed.
supClosed_sInter theorem
(hS : ∀ s ∈ S, SupClosed s) : SupClosed (⋂₀ S)
Full source 
lemma supClosed_sInter (hS : ∀ s ∈ S, SupClosed s) : SupClosed (⋂₀ S) :=
  fun _a ha _b hb _s hs ↦ hS _ hs (ha _ hs) (hb _ hs)
Intersection of Sup-Closed Sets is Sup-Closed
Informal description
For any family of sets $S$ in a type $\alpha$ with a join operation $\sqcup$, if every set $s \in S$ is sup-closed (i.e., for any $a, b \in s$, $a \sqcup b \in s$), then the intersection $\bigcap S$ is also sup-closed.
supClosed_iInter theorem
(hf : ∀ i, SupClosed (f i)) : SupClosed (⋂ i, f i)
Full source 
lemma supClosed_iInter (hf : ∀ i, SupClosed (f i)) : SupClosed (⋂ i, f i) :=
  supClosed_sInter <| forall_mem_range.2 hf
Intersection of a Family of Sup-Closed Sets is Sup-Closed
Informal description
For any family of sets $\{f_i\}_{i \in I}$ in a type $\alpha$ with a join operation $\sqcup$, if each set $f_i$ is sup-closed (i.e., for any $a, b \in f_i$, $a \sqcup b \in f_i$), then the intersection $\bigcap_{i \in I} f_i$ is also sup-closed.
IsUpperSet.supClosed theorem
(hs : IsUpperSet s) : SupClosed s
Full source 
lemma IsUpperSet.supClosed (hs : IsUpperSet s) : SupClosed s := fun _a _ _b ↦ hs le_sup_right
Upper sets are sup-closed
Informal description
If a set $s$ in a partially ordered set is an upper set (i.e., for any $x \in s$ and $y \geq x$, we have $y \in s$), then $s$ is sup-closed (i.e., for any $a, b \in s$, their join $a \sqcup b$ belongs to $s$).
SupClosed.preimage theorem
[FunLike F β α] [SupHomClass F β α] (hs : SupClosed s) (f : F) : SupClosed (f ⁻¹' s)
Full source 
lemma SupClosed.preimage [FunLike F β α] [SupHomClass F β α] (hs : SupClosed s) (f : F) :
    SupClosed (f ⁻¹' s) :=
  fun a ha b hb ↦ by simpa [map_sup] using hs ha hb
Preimage of Sup-Closed Set under Supremum-Preserving Map is Sup-Closed
Informal description
Let $F$ be a type of functions from $\beta$ to $\alpha$ that preserves suprema (i.e., for any $f \in F$ and $x, y \in \beta$, $f(x \sqcup y) = f(x) \sqcup f(y)$). If $s$ is a sup-closed subset of $\alpha$ (i.e., for any $a, b \in s$, $a \sqcup b \in s$), then the preimage $f^{-1}(s)$ is a sup-closed subset of $\beta$.
SupClosed.image theorem
[FunLike F α β] [SupHomClass F α β] (hs : SupClosed s) (f : F) : SupClosed (f '' s)
Full source 
lemma SupClosed.image [FunLike F α β] [SupHomClass F α β] (hs : SupClosed s) (f : F) :
    SupClosed (f '' s) := by
  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩
  rw [← map_sup]
  exact Set.mem_image_of_mem _ <| hs ha hb
Image of a Sup-Closed Set under a Supremum-Preserving Map is Sup-Closed
Informal description
Let $F$ be a type of functions from $\alpha$ to $\beta$ that preserves suprema (i.e., for any $f \in F$ and $x, y \in \alpha$, $f(x \sqcup y) = f(x) \sqcup f(y)$). If $s$ is a sup-closed subset of $\alpha$ (i.e., for any $a, b \in s$, $a \sqcup b \in s$), then the image $f(s)$ is a sup-closed subset of $\beta$.
supClosed_range theorem
[FunLike F α β] [SupHomClass F α β] (f : F) : SupClosed (Set.range f)
Full source 
lemma supClosed_range [FunLike F α β] [SupHomClass F α β] (f : F) : SupClosed (Set.range f) := by
  simpa using supClosed_univ.image f
Range of a Supremum-Preserving Map is Sup-Closed
Informal description
Let $F$ be a type of functions from $\alpha$ to $\beta$ that preserves suprema (i.e., for any $f \in F$ and $x, y \in \alpha$, $f(x \sqcup y) = f(x) \sqcup f(y)$). Then the range of any such function $f \in F$ is a sup-closed subset of $\beta$.
SupClosed.prod theorem
{t : Set β} (hs : SupClosed s) (ht : SupClosed t) : SupClosed (s ×ˢ t)
Full source 
lemma SupClosed.prod {t : Set β} (hs : SupClosed s) (ht : SupClosed t) : SupClosed (s ×ˢ t) :=
  fun _a ha _b hb ↦ ⟨hs ha.1 hb.1, ht ha.2 hb.2⟩
Sup-closedness is Preserved under Cartesian Product
Informal description
Let $s$ be a sup-closed subset of a type $\alpha$ with a join operation $\sqcup$, and let $t$ be a sup-closed subset of a type $\beta$ with a join operation $\sqcup$. Then the Cartesian product $s \times t$ is also sup-closed, where the join operation on $\alpha \times \beta$ is defined componentwise.
supClosed_pi theorem
{ι : Type*} {α : ι → Type*} [∀ i, SemilatticeSup (α i)] {s : Set ι} {t : ∀ i, Set (α i)} (ht : ∀ i ∈ s, SupClosed (t i)) : SupClosed (s.pi t)
Full source 
lemma supClosed_pi {ι : Type*} {α : ι → Type*} [∀ i, SemilatticeSup (α i)] {s : Set ι}
    {t : ∀ i, Set (α i)} (ht : ∀ i ∈ s, SupClosed (t i)) : SupClosed (s.pi t) :=
  fun _a ha _b hb _i hi ↦ ht _ hi (ha _ hi) (hb _ hi)
Sup-closedness of product sets in a family of join-semilattices
Informal description
Let $\{ \alpha_i \}_{i \in \iota}$ be a family of types, each equipped with a join-semilattice structure. Given a subset $s \subseteq \iota$ and for each $i \in s$, a sup-closed subset $t_i \subseteq \alpha_i$, then the product set $\prod_{i \in s} t_i$ is sup-closed in the product semilattice $\prod_{i \in s} \alpha_i$.
SupClosed.insert_upperBounds theorem
{s : Set α} {a : α} (hs : SupClosed s) (ha : a ∈ upperBounds s) : SupClosed (insert a s)
Full source 
lemma SupClosed.insert_upperBounds {s : Set α} {a : α} (hs : SupClosed s) (ha : a ∈ upperBounds s) :
    SupClosed (insert a s) := by
  rw [SupClosed]
  aesop
Insertion of an Upper Bound Preserves Sup-Closed Property
Informal description
Let $s$ be a sup-closed subset of a type $\alpha$ with a join operation $\sqcup$, and let $a \in \alpha$ be an upper bound of $s$. Then the set obtained by inserting $a$ into $s$, denoted by $\{a\} \cup s$, is also sup-closed.
SupClosed.insert_lowerBounds theorem
{s : Set α} {a : α} (h : SupClosed s) (ha : a ∈ lowerBounds s) : SupClosed (insert a s)
Full source 
lemma SupClosed.insert_lowerBounds {s : Set α} {a : α} (h : SupClosed s) (ha : a ∈ lowerBounds s) :
    SupClosed (insert a s) := by
  rw [SupClosed]
  have ha' : ∀ b ∈ s, a ≤ b := fun _ a ↦ ha a
  aesop
Insertion of Lower Bound Preserves Sup-Closed Property
Informal description
Let $s$ be a sup-closed subset of a type $\alpha$ with a join operation $\sqcup$, and let $a$ be an element in the lower bounds of $s$. Then the set obtained by inserting $a$ into $s$ is also sup-closed.
SupClosed.finsetSup'_mem theorem
(hs : SupClosed s) (ht : t.Nonempty) : (∀ i ∈ t, f i ∈ s) → t.sup' ht f ∈ s
Full source 
lemma SupClosed.finsetSup'_mem (hs : SupClosed s) (ht : t.Nonempty) :
    (∀ i ∈ t, f i ∈ s) → t.sup' ht f ∈ s :=
  sup'_induction _ _ hs
Sup-closed sets are closed under finite nonempty joins
Informal description
Let $s$ be a sup-closed subset of a type $\alpha$ with a join operation $\sqcup$, and let $t$ be a nonempty finite set. If a function $f$ maps every element of $t$ into $s$, then the join (supremum) of $f$ over $t$ is also in $s$. In other words, if $\forall i \in t, f(i) \in s$, then $\bigsqcup_{i \in t} f(i) \in s$.
SupClosed.finsetSup_mem theorem
[OrderBot α] (hs : SupClosed s) (ht : t.Nonempty) : (∀ i ∈ t, f i ∈ s) → t.sup f ∈ s
Full source 
lemma SupClosed.finsetSup_mem [OrderBot α] (hs : SupClosed s) (ht : t.Nonempty) :
    (∀ i ∈ t, f i ∈ s) → t.sup f ∈ s :=
  sup'_eq_sup ht f ▸ hs.finsetSup'_mem ht
Sup-closed sets are closed under finite nonempty joins (with bottom element)
Informal description
Let $\alpha$ be a type with a join operation $\sqcup$ and a least element $\bot$. For any sup-closed subset $s \subseteq \alpha$ and any nonempty finite set $t$, if a function $f$ satisfies $f(i) \in s$ for all $i \in t$, then the join $\bigsqcup_{i \in t} f(i)$ is also in $s$.
InfClosed definition
(s : Set α) : Prop
Full source 
/-- A set `s` is *inf-closed* if `a ⊓ b ∈ s` for all `a ∈ s`, `b ∈ s`. -/
def InfClosed (s : Set α) : Prop := ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → a ⊓ ba ⊓ b ∈ s
Inf-closed set
Informal description
A set $s$ in a type $\alpha$ is called *inf-closed* if for any elements $a, b \in s$, their meet $a \sqcap b$ is also in $s$.
infClosed_empty theorem
: InfClosed (∅ : Set α)
Full source 
@[simp] lemma infClosed_empty : InfClosed (∅ : Set α) := by simp [InfClosed]
Empty Set is Inf-Closed
Informal description
The empty set is inf-closed in any type $\alpha$ equipped with a meet operation $\sqcap$.
infClosed_singleton theorem
: InfClosed ({ a } : Set α)
Full source 
@[simp] lemma infClosed_singleton : InfClosed ({a} : Set α) := by simp [InfClosed]
Singleton Sets are Inf-Closed
Informal description
For any element $a$ in a type $\alpha$ equipped with a meet operation $\sqcap$, the singleton set $\{a\}$ is inf-closed.
infClosed_univ theorem
: InfClosed (univ : Set α)
Full source 
@[simp] lemma infClosed_univ : InfClosed (univ : Set α) := by simp [InfClosed]
Universal Set is Inf-Closed
Informal description
The universal set (containing all elements of type $\alpha$) is inf-closed, meaning that for any two elements $a, b \in \alpha$, their meet $a \sqcap b$ is also in $\alpha$.
InfClosed.inter theorem
(hs : InfClosed s) (ht : InfClosed t) : InfClosed (s ∩ t)
Full source 
lemma InfClosed.inter (hs : InfClosed s) (ht : InfClosed t) : InfClosed (s ∩ t) :=
  fun _a ha _b hb ↦ ⟨hs ha.1 hb.1, ht ha.2 hb.2⟩
Intersection of Inf-Closed Sets is Inf-Closed
Informal description
If two sets $s$ and $t$ in a type $\alpha$ are inf-closed, then their intersection $s \cap t$ is also inf-closed.
infClosed_sInter theorem
(hS : ∀ s ∈ S, InfClosed s) : InfClosed (⋂₀ S)
Full source 
lemma infClosed_sInter (hS : ∀ s ∈ S, InfClosed s) : InfClosed (⋂₀ S) :=
  fun _a ha _b hb _s hs ↦ hS _ hs (ha _ hs) (hb _ hs)
Intersection of Inf-Closed Sets is Inf-Closed
Informal description
For any family of sets $S$ in a type $\alpha$, if every set $s \in S$ is inf-closed, then the intersection $\bigcap_{s \in S} s$ is also inf-closed.
infClosed_iInter theorem
(hf : ∀ i, InfClosed (f i)) : InfClosed (⋂ i, f i)
Full source 
lemma infClosed_iInter (hf : ∀ i, InfClosed (f i)) : InfClosed (⋂ i, f i) :=
  infClosed_sInter <| forall_mem_range.2 hf
Intersection of Inf-Closed Sets is Inf-Closed
Informal description
For any family of sets $\{f_i\}_{i \in I}$ in a type $\alpha$, if each set $f_i$ is inf-closed, then the intersection $\bigcap_{i \in I} f_i$ is also inf-closed.
InfClosed.codirectedOn theorem
(hs : InfClosed s) : DirectedOn (· ≥ ·) s
Full source 
lemma InfClosed.codirectedOn (hs : InfClosed s) : DirectedOn (· ≥ ·) s :=
  fun _a ha _b hb ↦ ⟨_, hs ha hb, inf_le_left, inf_le_right⟩
Inf-closed sets are codirected with respect to $\geq$
Informal description
For any inf-closed set $s$ in a meet-semilattice, the set $s$ is codirected with respect to the greater-than-or-equal relation $\geq$.
IsLowerSet.infClosed theorem
(hs : IsLowerSet s) : InfClosed s
Full source 
lemma IsLowerSet.infClosed (hs : IsLowerSet s) : InfClosed s := fun _a _ _b ↦ hs inf_le_right
Lower sets are inf-closed
Informal description
If a set $s$ in a type $\alpha$ is a lower set (i.e., for any $a \in s$ and $b \leq a$, we have $b \in s$), then $s$ is inf-closed (i.e., for any $a, b \in s$, their meet $a \sqcap b$ is also in $s$).
InfClosed.preimage theorem
[FunLike F β α] [InfHomClass F β α] (hs : InfClosed s) (f : F) : InfClosed (f ⁻¹' s)
Full source 
lemma InfClosed.preimage [FunLike F β α] [InfHomClass F β α] (hs : InfClosed s) (f : F) :
    InfClosed (f ⁻¹' s) :=
  fun a ha b hb ↦ by simpa [map_inf] using hs ha hb
Preimage of Inf-Closed Set under Infimum-Preserving Map is Inf-Closed
Informal description
Let $F$ be a type of functions from $\beta$ to $\alpha$ that preserves infima (i.e., for any $f \in F$ and $x, y \in \beta$, $f(x \sqcap y) = f(x) \sqcap f(y)$). If $s \subseteq \alpha$ is an inf-closed set, then the preimage $f^{-1}(s)$ is also inf-closed in $\beta$.
InfClosed.image theorem
[FunLike F α β] [InfHomClass F α β] (hs : InfClosed s) (f : F) : InfClosed (f '' s)
Full source 
lemma InfClosed.image [FunLike F α β] [InfHomClass F α β] (hs : InfClosed s) (f : F) :
    InfClosed (f '' s) := by
  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩
  rw [← map_inf]
  exact Set.mem_image_of_mem _ <| hs ha hb
Image of Inf-Closed Set under Infimum-Preserving Map is Inf-Closed
Informal description
Let $F$ be a type of functions from $\alpha$ to $\beta$ that preserves infima (i.e., for any $f \in F$ and $x, y \in \alpha$, $f(x \sqcap y) = f(x) \sqcap f(y)$). If $s \subseteq \alpha$ is an inf-closed set, then the image $f(s)$ is also inf-closed in $\beta$.
infClosed_range theorem
[FunLike F α β] [InfHomClass F α β] (f : F) : InfClosed (Set.range f)
Full source 
lemma infClosed_range [FunLike F α β] [InfHomClass F α β] (f : F) : InfClosed (Set.range f) := by
  simpa using infClosed_univ.image f
Range of Infimum-Preserving Map is Inf-Closed
Informal description
Let $F$ be a type of functions from $\alpha$ to $\beta$ that preserves infima (i.e., for any $f \in F$ and $x, y \in \alpha$, $f(x \sqcap y) = f(x) \sqcap f(y)$). Then the range of any function $f \in F$ is an inf-closed set in $\beta$.
InfClosed.prod theorem
{t : Set β} (hs : InfClosed s) (ht : InfClosed t) : InfClosed (s ×ˢ t)
Full source 
lemma InfClosed.prod {t : Set β} (hs : InfClosed s) (ht : InfClosed t) : InfClosed (s ×ˢ t) :=
  fun _a ha _b hb ↦ ⟨hs ha.1 hb.1, ht ha.2 hb.2⟩
Product of Inf-closed Sets is Inf-closed
Informal description
Let $s$ be an inf-closed set in a semilattice $\alpha$ and $t$ be an inf-closed set in a semilattice $\beta$. Then the Cartesian product $s \times t$ is inf-closed in $\alpha \times \beta$, meaning that for any $(a_1, b_1), (a_2, b_2) \in s \times t$, their meet $(a_1 \sqcap a_2, b_1 \sqcap b_2)$ is also in $s \times t$.
infClosed_pi theorem
{ι : Type*} {α : ι → Type*} [∀ i, SemilatticeInf (α i)] {s : Set ι} {t : ∀ i, Set (α i)} (ht : ∀ i ∈ s, InfClosed (t i)) : InfClosed (s.pi t)
Full source 
lemma infClosed_pi {ι : Type*} {α : ι → Type*} [∀ i, SemilatticeInf (α i)] {s : Set ι}
    {t : ∀ i, Set (α i)} (ht : ∀ i ∈ s, InfClosed (t i)) : InfClosed (s.pi t) :=
  fun _a ha _b hb _i hi ↦ ht _ hi (ha _ hi) (hb _ hi)
Inf-closed property of product sets in meet-semilattices
Informal description
Let $\{ \alpha_i \}_{i \in \iota}$ be a family of types, each equipped with a meet-semilattice structure. Given a subset $s \subseteq \iota$ and for each $i \in s$, a subset $t_i \subseteq \alpha_i$ that is inf-closed, then the product set $\prod_{i \in s} t_i$ is inf-closed in the product semilattice $\prod_{i \in s} \alpha_i$.
InfClosed.insert_upperBounds theorem
{s : Set α} {a : α} (hs : InfClosed s) (ha : a ∈ upperBounds s) : InfClosed (insert a s)
Full source 
lemma InfClosed.insert_upperBounds {s : Set α} {a : α} (hs : InfClosed s) (ha : a ∈ upperBounds s) :
    InfClosed (insert a s) := by
  rw [InfClosed]
  have ha' : ∀ b ∈ s, b ≤ a := fun _ a ↦ ha a
  aesop
Insertion of an Upper Bound Preserves Inf-Closed Property
Informal description
Let $s$ be an inf-closed set in a semilattice $\alpha$, and let $a \in \alpha$ be an upper bound of $s$. Then the set obtained by inserting $a$ into $s$, denoted by $\{a\} \cup s$, is also inf-closed.
InfClosed.insert_lowerBounds theorem
{s : Set α} {a : α} (h : InfClosed s) (ha : a ∈ lowerBounds s) : InfClosed (insert a s)
Full source 
lemma InfClosed.insert_lowerBounds {s : Set α} {a : α} (h : InfClosed s) (ha : a ∈ lowerBounds s) :
    InfClosed (insert a s) := by
  rw [InfClosed]
  aesop
Insertion of a Lower Bound Preserves Inf-Closed Property
Informal description
Let $s$ be an inf-closed set in a type $\alpha$ with a meet-semilattice structure, and let $a \in \alpha$ be a lower bound of $s$. Then the set obtained by inserting $a$ into $s$, denoted by $\{a\} \cup s$, is also inf-closed.
InfClosed.finsetInf'_mem theorem
(hs : InfClosed s) (ht : t.Nonempty) : (∀ i ∈ t, f i ∈ s) → t.inf' ht f ∈ s
Full source 
lemma InfClosed.finsetInf'_mem (hs : InfClosed s) (ht : t.Nonempty) :
    (∀ i ∈ t, f i ∈ s) → t.inf' ht f ∈ s :=
  inf'_induction _ _ hs
Infimum of a Finite Family in an Inf-Closed Set
Informal description
Let $s$ be an inf-closed set in a type $\alpha$, and let $t$ be a nonempty finite set. If for every element $i \in t$, the value $f(i)$ belongs to $s$, then the infimum of $f$ over $t$ (denoted as $t.\inf'\, f$) also belongs to $s$.
InfClosed.finsetInf_mem theorem
[OrderTop α] (hs : InfClosed s) (ht : t.Nonempty) : (∀ i ∈ t, f i ∈ s) → t.inf f ∈ s
Full source 
lemma InfClosed.finsetInf_mem [OrderTop α] (hs : InfClosed s) (ht : t.Nonempty) :
    (∀ i ∈ t, f i ∈ s) → t.inf f ∈ s :=
  inf'_eq_inf ht f ▸ hs.finsetInf'_mem ht
Infimum of a Finite Family in an Inf-Closed Set with Top Element
Informal description
Let $\alpha$ be a type with an order and a top element $\top$, and let $s$ be an inf-closed subset of $\alpha$. For any nonempty finite set $t$ and any function $f$ from $t$ to $\alpha$, if $f(i) \in s$ for all $i \in t$, then the infimum of $f$ over $t$ (denoted $\inf_{i \in t} f(i)$) is also in $s$.
IsSublattice structure
(s : Set α)
Full source 
/-- 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`. -/
structure IsSublattice (s : Set α) : Prop where
  supClosed : SupClosed s
  infClosed : InfClosed s
Sublattice
Informal description
A subset $s$ of a lattice is called a *sublattice* if it is closed under both join ($\sqcup$) and meet ($\sqcap$), meaning that for any two elements $a, b \in s$, their join $a \sqcup b$ and meet $a \sqcap b$ also belong to $s$.
isSublattice_univ theorem
: IsSublattice (Set.univ : Set α)
Full source 
@[simp] lemma isSublattice_univ : IsSublattice (Set.univ : Set α) :=
  ⟨supClosed_univ, infClosed_univ⟩
Universal Set is a Sublattice
Informal description
The universal set (containing all elements of a lattice $\alpha$) is a sublattice, meaning it is closed under both join ($\sqcup$) and meet ($\sqcap$) operations.
isSublattice_sInter theorem
(hS : ∀ s ∈ S, IsSublattice s) : IsSublattice (⋂₀ S)
Full source 
lemma isSublattice_sInter (hS : ∀ s ∈ S, IsSublattice s) : IsSublattice (⋂₀ S) :=
  ⟨supClosed_sInter fun _s hs ↦ (hS _ hs).1, infClosed_sInter fun _s hs ↦ (hS _ hs).2⟩
Intersection of Sublattices is a Sublattice
Informal description
For any family of sets $S$ in a lattice $\alpha$, if every set $s \in S$ is a sublattice (i.e., closed under both join $\sqcup$ and meet $\sqcap$), then the intersection $\bigcap_{s \in S} s$ is also a sublattice.
isSublattice_iInter theorem
(hf : ∀ i, IsSublattice (f i)) : IsSublattice (⋂ i, f i)
Full source 
lemma isSublattice_iInter (hf : ∀ i, IsSublattice (f i)) : IsSublattice (⋂ i, f i) :=
  ⟨supClosed_iInter fun _i ↦ (hf _).1, infClosed_iInter fun _i ↦ (hf _).2⟩
Intersection of Sublattices is a Sublattice
Informal description
For any family of sets $\{f_i\}_{i \in I}$ in a lattice $\alpha$, if each set $f_i$ is a sublattice (i.e., closed under both join $\sqcup$ and meet $\sqcap$), then the intersection $\bigcap_{i \in I} f_i$ is also a sublattice.
IsSublattice.preimage theorem
[FunLike F β α] [LatticeHomClass F β α] (hs : IsSublattice s) (f : F) : IsSublattice (f ⁻¹' s)
Full source 
lemma IsSublattice.preimage [FunLike F β α] [LatticeHomClass F β α]
    (hs : IsSublattice s) (f : F) :
    IsSublattice (f ⁻¹' s) := ⟨hs.1.preimage _, hs.2.preimage _⟩
Preimage of a Sublattice under a Lattice Homomorphism is a Sublattice
Informal description
Let $F$ be a type of functions from $\beta$ to $\alpha$ that are lattice homomorphisms (i.e., preserve both suprema $\sqcup$ and infima $\sqcap$). If $s \subseteq \alpha$ is a sublattice (closed under both $\sqcup$ and $\sqcap$), then the preimage $f^{-1}(s) \subseteq \beta$ under any $f \in F$ is also a sublattice.
IsSublattice.image theorem
[FunLike F α β] [LatticeHomClass F α β] (hs : IsSublattice s) (f : F) : IsSublattice (f '' s)
Full source 
lemma IsSublattice.image [FunLike F α β] [LatticeHomClass F α β] (hs : IsSublattice s) (f : F) :
    IsSublattice (f '' s) := ⟨hs.1.image _, hs.2.image _⟩
Image of a Sublattice under a Lattice Homomorphism is a Sublattice
Informal description
Let $\alpha$ and $\beta$ be lattices, and let $F$ be a type of lattice homomorphisms from $\alpha$ to $\beta$. For any sublattice $s$ of $\alpha$ (i.e., a subset closed under both join $\sqcup$ and meet $\sqcap$) and any lattice homomorphism $f \in F$, the image $f(s)$ is a sublattice of $\beta$.
IsSublattice_range theorem
[FunLike F α β] [LatticeHomClass F α β] (f : F) : IsSublattice (Set.range f)
Full source 
lemma IsSublattice_range [FunLike F α β] [LatticeHomClass F α β] (f : F) :
    IsSublattice (Set.range f) :=
  ⟨supClosed_range _, infClosed_range _⟩
Range of a Lattice Homomorphism is a Sublattice
Informal description
Let $\alpha$ and $\beta$ be lattices, and let $F$ be a type of lattice homomorphisms from $\alpha$ to $\beta$. For any lattice homomorphism $f \in F$, the range of $f$ is a sublattice of $\beta$, meaning that for any two elements $y_1, y_2$ in the range of $f$, their join $y_1 \sqcup y_2$ and meet $y_1 \sqcap y_2$ also belong to the range of $f$.
IsSublattice.prod theorem
{t : Set β} (hs : IsSublattice s) (ht : IsSublattice t) : IsSublattice (s ×ˢ t)
Full source 
lemma IsSublattice.prod {t : Set β} (hs : IsSublattice s) (ht : IsSublattice t) :
    IsSublattice (s ×ˢ t) := ⟨hs.1.prod ht.1, hs.2.prod ht.2⟩
Product of Sublattices is a Sublattice
Informal description
Let $s$ be a sublattice of a lattice $\alpha$ and $t$ be a sublattice of a lattice $\beta$. Then the Cartesian product $s \times t$ is a sublattice of the product lattice $\alpha \times \beta$, meaning that for any $(a_1, b_1), (a_2, b_2) \in s \times t$, both their join $(a_1 \sqcup a_2, b_1 \sqcup b_2)$ and meet $(a_1 \sqcap a_2, b_1 \sqcap b_2)$ belong to $s \times t$.
isSublattice_pi theorem
{ι : Type*} {α : ι → Type*} [∀ i, Lattice (α i)] {s : Set ι} {t : ∀ i, Set (α i)} (ht : ∀ i ∈ s, IsSublattice (t i)) : IsSublattice (s.pi t)
Full source 
lemma isSublattice_pi {ι : Type*} {α : ι → Type*} [∀ i, Lattice (α i)] {s : Set ι}
    {t : ∀ i, Set (α i)} (ht : ∀ i ∈ s, IsSublattice (t i)) : IsSublattice (s.pi t) :=
  ⟨supClosed_pi fun _i hi ↦ (ht _ hi).1, infClosed_pi fun _i hi ↦ (ht _ hi).2⟩
Product of Sublattices is a Sublattice
Informal description
Let $\{ \alpha_i \}_{i \in \iota}$ be a family of types, each equipped with a lattice structure. Given a subset $s \subseteq \iota$ and for each $i \in s$, a sublattice $t_i \subseteq \alpha_i$, then the product set $\prod_{i \in s} t_i$ is a sublattice of the product lattice $\prod_{i \in s} \alpha_i$.
supClosed_preimage_toDual theorem
{s : Set αᵒᵈ} : SupClosed (toDual ⁻¹' s) ↔ InfClosed s
Full source 
@[simp] lemma supClosed_preimage_toDual {s : Set αᵒᵈ} :
    SupClosedSupClosed (toDual ⁻¹' s) ↔ InfClosed s := Iff.rfl
Sup-closed Preimage of Dual Set is Equivalent to Inf-closed Set
Informal description
For any subset $s$ of the order dual $\alpha^\mathrm{op}$ of a type $\alpha$, the preimage of $s$ under the order isomorphism $\mathrm{toDual} : \alpha \to \alpha^\mathrm{op}$ is sup-closed if and only if $s$ is inf-closed. In other words, the set $\mathrm{toDual}^{-1}(s)$ is closed under the join operation $\sqcup$ in $\alpha$ precisely when $s$ is closed under the meet operation $\sqcap$ in $\alpha^\mathrm{op}$.
infClosed_preimage_toDual theorem
{s : Set αᵒᵈ} : InfClosed (toDual ⁻¹' s) ↔ SupClosed s
Full source 
@[simp] lemma infClosed_preimage_toDual {s : Set αᵒᵈ} :
    InfClosedInfClosed (toDual ⁻¹' s) ↔ SupClosed s := Iff.rfl
Inf-closed Preimage under Order-Dual is Equivalent to Sup-closed Set
Informal description
For any subset $s$ of the order dual $\alpha^\mathrm{op}$ of a type $\alpha$, the preimage of $s$ under the order isomorphism $\mathrm{toDual} : \alpha \to \alpha^\mathrm{op}$ is inf-closed if and only if $s$ is sup-closed. In other words, the set $\mathrm{toDual}^{-1}(s)$ is closed under the meet operation $\sqcap$ in $\alpha$ precisely when $s$ is closed under the join operation $\sqcup$ in $\alpha^\mathrm{op}$.
supClosed_preimage_ofDual theorem
{s : Set α} : SupClosed (ofDual ⁻¹' s) ↔ InfClosed s
Full source 
@[simp] lemma supClosed_preimage_ofDual {s : Set α} :
    SupClosedSupClosed (ofDual ⁻¹' s) ↔ InfClosed s := Iff.rfl
Sup-closed Preimage under Order-Dual is Equivalent to Inf-closed Set
Informal description
For any subset $s$ of a lattice $\alpha$, the preimage of $s$ under the order-dual map $\mathrm{ofDual} : \alpha^\mathrm{op} \to \alpha$ is sup-closed if and only if $s$ is inf-closed. In other words, for all $a, b \in \alpha^\mathrm{op}$, if $\mathrm{ofDual}(a), \mathrm{ofDual}(b) \in s$ implies $\mathrm{ofDual}(a \sqcup b) \in s$, then for all $x, y \in \alpha$, $x, y \in s$ implies $x \sqcap y \in s$, and vice versa.
infClosed_preimage_ofDual theorem
{s : Set α} : InfClosed (ofDual ⁻¹' s) ↔ SupClosed s
Full source 
@[simp] lemma infClosed_preimage_ofDual {s : Set α} :
    InfClosedInfClosed (ofDual ⁻¹' s) ↔ SupClosed s := Iff.rfl
Inf-closed Preimage under Order-Dual is Equivalent to Sup-closed Set
Informal description
For any subset $s$ of a lattice $\alpha$, the preimage of $s$ under the order-dual map $\text{ofDual} : \alpha^\text{op} \to \alpha$ is inf-closed if and only if $s$ is sup-closed. In other words, for all $a, b \in \alpha^\text{op}$, if $\text{ofDual}(a), \text{ofDual}(b) \in s$ implies $\text{ofDual}(a \sqcap b) \in s$, then for all $x, y \in \alpha$, $x, y \in s$ implies $x \sqcup y \in s$, and vice versa.
isSublattice_preimage_toDual theorem
{s : Set αᵒᵈ} : IsSublattice (toDual ⁻¹' s) ↔ IsSublattice s
Full source 
@[simp] lemma isSublattice_preimage_toDual {s : Set αᵒᵈ} :
    IsSublatticeIsSublattice (toDual ⁻¹' s) ↔ IsSublattice s := ⟨fun h ↦ ⟨h.2, h.1⟩, fun h ↦ ⟨h.2, h.1⟩⟩
Sublattice Property under Order-Dual Preimage via $\text{toDual}$
Informal description
For any subset $s$ of the order-dual lattice $\alpha^\text{op}$, the preimage of $s$ under the order-dual map $\text{toDual} : \alpha \to \alpha^\text{op}$ is a sublattice of $\alpha$ if and only if $s$ is a sublattice of $\alpha^\text{op}$. In other words, $s$ is closed under both join ($\sqcup$) and meet ($\sqcap$) in $\alpha^\text{op}$ if and only if its preimage under $\text{toDual}$ is closed under both operations in $\alpha$.
isSublattice_preimage_ofDual theorem
: IsSublattice (ofDual ⁻¹' s) ↔ IsSublattice s
Full source 
@[simp] lemma isSublattice_preimage_ofDual :
    IsSublatticeIsSublattice (ofDual ⁻¹' s) ↔ IsSublattice s := ⟨fun h ↦ ⟨h.2, h.1⟩, fun h ↦ ⟨h.2, h.1⟩⟩
Sublattice Property under Order-Dual Preimage
Informal description
For any subset $s$ of a lattice $\alpha$, the preimage of $s$ under the order-dual map $\text{ofDual} : \alpha^\text{op} \to \alpha$ is a sublattice if and only if $s$ itself is a sublattice. In other words, $s$ is closed under both join ($\sqcup$) and meet ($\sqcap$) in $\alpha^\text{op}$ if and only if it is closed under both operations in $\alpha$.
LinearOrder.supClosed theorem
(s : Set α) : SupClosed s
Full source 
@[simp] protected lemma LinearOrder.supClosed (s : Set α) : SupClosed s :=
  fun a ha b hb ↦ by cases le_total a b <;> simp [*]
Sup-closed Property of Subsets in Linear Orders
Informal description
For any subset $s$ of a linearly ordered type $\alpha$, the set $s$ is sup-closed, meaning that for any two elements $a, b \in s$, their supremum $a \sqcup b$ is also in $s$.
LinearOrder.infClosed theorem
(s : Set α) : InfClosed s
Full source 
@[simp] protected lemma LinearOrder.infClosed (s : Set α) : InfClosed s :=
  fun a ha b hb ↦ by cases le_total a b <;> simp [*]
Every subset in a linear order is inf-closed
Informal description
In a linearly ordered set $\alpha$, every subset $s \subseteq \alpha$ is inf-closed, meaning that for any two elements $a, b \in s$, their meet $a \sqcap b$ (which is $\min(a, b)$ in a linear order) is also in $s$.
LinearOrder.isSublattice theorem
(s : Set α) : IsSublattice s
Full source 
@[simp] protected lemma LinearOrder.isSublattice (s : Set α) : IsSublattice s :=
  ⟨LinearOrder.supClosed _, LinearOrder.infClosed _⟩
Every subset in a linear order is a sublattice
Informal description
For any subset $s$ of a linearly ordered type $\alpha$, the set $s$ is a sublattice, meaning it is closed under both join ($\sqcup$) and meet ($\sqcap$). In other words, for any two elements $a, b \in s$, their supremum $a \sqcup b$ and infimum $a \sqcap b$ (which correspond to $\max(a, b)$ and $\min(a, b)$ in a linear order) also belong to $s$.
supClosure definition
: ClosureOperator (Set α)
Full source 
/-- Every set in a join-semilattice generates a set closed under join. -/
@[simps! isClosed]
def supClosure : ClosureOperator (Set α) := .ofPred
  (fun s ↦ {a | ∃ (t : Finset α) (ht : t.Nonempty), ↑t ⊆ s ∧ t.sup' ht id = a})
  SupClosed
  (fun s a ha ↦ ⟨{a}, singleton_nonempty _, by simpa⟩)
  (by
    classical
    rintro s _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩
    refine ⟨_, ht.mono subset_union_left, ?_, sup'_union ht hu _⟩
    rw [coe_union]
    exact Set.union_subset hts hus)
  (by rintro s₁ s₂ hs h₂ _ ⟨t, ht, hts, rfl⟩; exact h₂.finsetSup'_mem ht fun i hi ↦ hs <| hts hi)
Sup-closure of a set
Informal description
The *sup-closure* of a subset $s$ in a join-semilattice is the smallest sup-closed set containing $s$. It consists of all elements that can be expressed as the join of a nonempty finite subset of $s$.
subset_supClosure theorem
{s : Set α} : s ⊆ supClosure s
Full source 
@[simp] lemma subset_supClosure {s : Set α} : s ⊆ supClosure s := supClosure.le_closure _
Subset Property of Sup-Closure
Informal description
For any subset $s$ of a join-semilattice, $s$ is contained in its sup-closure, i.e., $s \subseteq \text{supClosure}(s)$.
supClosed_supClosure theorem
: SupClosed (supClosure s)
Full source 
@[simp] lemma supClosed_supClosure : SupClosed (supClosure s) := supClosure.isClosed_closure _
Sup-closure is Sup-closed
Informal description
The sup-closure of any subset $s$ in a join-semilattice is sup-closed, i.e., for any two elements $a, b \in \text{supClosure}(s)$, their join $a \sqcup b$ is also in $\text{supClosure}(s)$.
supClosure_mono theorem
: Monotone (supClosure : Set α → Set α)
Full source 
lemma supClosure_mono : Monotone (supClosure : Set α → Set α) := supClosure.monotone
Monotonicity of Sup-Closure Operator
Informal description
The sup-closure operator is monotone, meaning that for any two subsets $s$ and $t$ of a join-semilattice, if $s \subseteq t$, then $\text{supClosure}(s) \subseteq \text{supClosure}(t)$.
supClosure_eq_self theorem
: supClosure s = s ↔ SupClosed s
Full source 
@[simp] lemma supClosure_eq_self : supClosuresupClosure s = s ↔ SupClosed s := supClosure.isClosed_iff.symm
Characterization of Sup-Closed Sets via Sup-Closure
Informal description
For any subset $s$ of a join-semilattice $\alpha$, the sup-closure of $s$ equals $s$ if and only if $s$ is sup-closed (i.e., for any $a, b \in s$, their join $a \sqcup b$ is also in $s$).
supClosure_idem theorem
(s : Set α) : supClosure (supClosure s) = supClosure s
Full source 
lemma supClosure_idem (s : Set α) : supClosure (supClosure s) = supClosure s :=
  supClosure.idempotent _
Idempotence of Sup-closure Operation
Informal description
For any subset $s$ of a join-semilattice $\alpha$, the sup-closure of the sup-closure of $s$ is equal to the sup-closure of $s$, i.e., $\text{supClosure}(\text{supClosure}(s)) = \text{supClosure}(s)$.
supClosure_empty theorem
: supClosure (∅ : Set α) = ∅
Full source 
@[simp] lemma supClosure_empty : supClosure (∅ : Set α) = ∅ := by simp
Sup-closure of Empty Set is Empty
Informal description
The sup-closure of the empty set in a join-semilattice $\alpha$ is the empty set itself, i.e., $\text{supClosure}(\emptyset) = \emptyset$.
supClosure_singleton theorem
: supClosure { a } = { a }
Full source 
@[simp] lemma supClosure_singleton : supClosure {a} = {a} := by simp
Sup-closure of a singleton set is itself
Informal description
For any element $a$ in a join-semilattice $\alpha$, the sup-closure of the singleton set $\{a\}$ is $\{a\}$ itself.
supClosure_univ theorem
: supClosure (Set.univ : Set α) = Set.univ
Full source 
@[simp] lemma supClosure_univ : supClosure (Set.univ : Set α) = Set.univ := by simp
Sup-closure of Universal Set is Universal
Informal description
The sup-closure of the universal set in a join-semilattice $\alpha$ is the universal set itself, i.e., $\text{supClosure}(\text{univ}) = \text{univ}$.
upperBounds_supClosure theorem
(s : Set α) : upperBounds (supClosure s) = upperBounds s
Full source 
@[simp] lemma upperBounds_supClosure (s : Set α) : upperBounds (supClosure s) = upperBounds s :=
  (upperBounds_mono_set subset_supClosure).antisymm <| by
    rintro a ha _ ⟨t, ht, hts, rfl⟩
    exact sup'_le _ _ fun b hb ↦ ha <| hts hb
Upper Bounds of Sup-Closure Equal Upper Bounds of Original Set
Informal description
For any subset $s$ of a join-semilattice $\alpha$, the set of upper bounds of the sup-closure of $s$ is equal to the set of upper bounds of $s$, i.e., $\text{upperBounds}(\text{supClosure}(s)) = \text{upperBounds}(s)$.
isLUB_supClosure theorem
: IsLUB (supClosure s) a ↔ IsLUB s a
Full source 
@[simp] lemma isLUB_supClosure : IsLUBIsLUB (supClosure s) a ↔ IsLUB s a := by simp [IsLUB]
Least Upper Bound of Sup-Closure Equals Least Upper Bound of Original Set
Informal description
For any subset $s$ of a join-semilattice $\alpha$ and any element $a \in \alpha$, $a$ is the least upper bound of the sup-closure of $s$ if and only if $a$ is the least upper bound of $s$. In other words, $\text{IsLUB}(\text{supClosure}(s), a) \leftrightarrow \text{IsLUB}(s, a)$.
finsetSup'_mem_supClosure theorem
{ι : Type*} {t : Finset ι} (ht : t.Nonempty) {f : ι → α} (hf : ∀ i ∈ t, f i ∈ s) : t.sup' ht f ∈ supClosure s
Full source 
lemma finsetSup'_mem_supClosure {ι : Type*} {t : Finset ι} (ht : t.Nonempty) {f : ι → α}
    (hf : ∀ i ∈ t, f i ∈ s) : t.sup' ht f ∈ supClosure s :=
  supClosed_supClosure.finsetSup'_mem _ fun _i hi ↦ subset_supClosure <| hf _ hi
Finite Nonempty Joins in Sup-closure
Informal description
Let $s$ be a subset of a join-semilattice $\alpha$, and let $t$ be a nonempty finite set indexed by a type $\iota$. If a function $f \colon \iota \to \alpha$ maps every element of $t$ into $s$, then the join (supremum) of $f$ over $t$ is contained in the sup-closure of $s$, i.e., $\bigsqcup_{i \in t} f(i) \in \text{supClosure}(s)$.
supClosure_min theorem
: s ⊆ t → SupClosed t → supClosure s ⊆ t
Full source 
lemma supClosure_min : s ⊆ t → SupClosed t → supClosuresupClosure s ⊆ t := supClosure.closure_min
Minimality of Sup-closure: $\text{supClosure}(s) \subseteq t$ if $s \subseteq t$ and $t$ is sup-closed
Informal description
For any subsets $s$ and $t$ of a join-semilattice, if $s$ is contained in $t$ and $t$ is sup-closed, then the sup-closure of $s$ is also contained in $t$.
Set.Finite.supClosure theorem
(hs : s.Finite) : (supClosure s).Finite
Full source 
/-- The semilatice generated by a finite set is finite. -/
protected lemma Set.Finite.supClosure (hs : s.Finite) : (supClosure s).Finite := by
  lift s to Finset α using hs
  classical
  refine ({t ∈ s.powerset | t.Nonempty}.attach.image
    fun t ↦ t.1.sup' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_
  rintro _ ⟨t, ht, hts, rfl⟩
  simp only [id_eq, coe_image, mem_image, mem_coe, mem_attach, true_and, Subtype.exists,
    Finset.mem_powerset, Finset.not_nonempty_iff_eq_empty, mem_filter]
  exact ⟨t, ⟨hts, ht⟩, rfl⟩
Finiteness of Sup-closure for Finite Sets
Informal description
For any finite subset $s$ of a join-semilattice, the sup-closure of $s$ is also finite.
supClosure_prod theorem
(s : Set α) (t : Set β) : supClosure (s ×ˢ t) = supClosure s ×ˢ supClosure t
Full source 
@[simp] lemma supClosure_prod (s : Set α) (t : Set β) :
    supClosure (s ×ˢ t) = supClosure s ×ˢ supClosure t :=
  le_antisymm (supClosure_min (Set.prod_mono subset_supClosure subset_supClosure) <|
    supClosed_supClosure.prod supClosed_supClosure) <| by
      rintro ⟨_, _⟩ ⟨⟨u, hu, hus, rfl⟩, v, hv, hvt, rfl⟩
      refine ⟨u ×ˢ v, hu.product hv, ?_, ?_⟩
      · simpa only [coe_product] using Set.prod_mono hus hvt
      · simp [prodMk_sup'_sup']
Sup-closure of Cartesian Product Equals Product of Sup-closures
Informal description
For any subsets $s$ of a type $\alpha$ and $t$ of a type $\beta$, the sup-closure of their Cartesian product $s \times t$ is equal to the Cartesian product of their individual sup-closures, i.e., $\text{supClosure}(s \times t) = \text{supClosure}(s) \times \text{supClosure}(t)$.
infClosure definition
: ClosureOperator (Set α)
Full source 
/-- Every set in a join-semilattice generates a set closed under join. -/
@[simps! isClosed]
def infClosure : ClosureOperator (Set α) := ClosureOperator.ofPred
  (fun s ↦ {a | ∃ (t : Finset α) (ht : t.Nonempty), ↑t ⊆ s ∧ t.inf' ht id = a})
  InfClosed
  (fun s a ha ↦ ⟨{a}, singleton_nonempty _, by simpa⟩)
  (by
    classical
    rintro s _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩
    refine ⟨_, ht.mono subset_union_left, ?_, inf'_union ht hu _⟩
    rw [coe_union]
    exact Set.union_subset hts hus)
  (by rintro s₁ s₂ hs h₂ _ ⟨t, ht, hts, rfl⟩; exact h₂.finsetInf'_mem ht fun i hi ↦ hs <| hts hi)
Inf-closure of a set
Informal description
The *inf-closure* of a set $s$ in a meet-semilattice is the smallest inf-closed set containing $s$. It consists of all elements that can be expressed as the meet of a nonempty finite subset of $s$.
subset_infClosure theorem
{s : Set α} : s ⊆ infClosure s
Full source 
@[simp] lemma subset_infClosure {s : Set α} : s ⊆ infClosure s := infClosure.le_closure _
Set is Subset of its Inf-closure
Informal description
For any set $s$ in a meet-semilattice, $s$ is a subset of its inf-closure, i.e., $s \subseteq \text{infClosure}(s)$.
infClosed_infClosure theorem
: InfClosed (infClosure s)
Full source 
@[simp] lemma infClosed_infClosure : InfClosed (infClosure s) := infClosure.isClosed_closure _
Inf-closure is Inf-closed
Informal description
For any set $s$ in a meet-semilattice, its inf-closure $\text{infClosure}(s)$ is inf-closed, meaning that for any $a, b \in \text{infClosure}(s)$, their meet $a \sqcap b$ is also in $\text{infClosure}(s)$.
infClosure_mono theorem
: Monotone (infClosure : Set α → Set α)
Full source 
lemma infClosure_mono : Monotone (infClosure : Set α → Set α) := infClosure.monotone
Monotonicity of Inf-closure Operator
Informal description
The inf-closure operator is monotone, meaning that for any two sets $s$ and $t$ in a meet-semilattice, if $s \subseteq t$, then $\text{infClosure}(s) \subseteq \text{infClosure}(t)$.
infClosure_eq_self theorem
: infClosure s = s ↔ InfClosed s
Full source 
@[simp] lemma infClosure_eq_self : infClosureinfClosure s = s ↔ InfClosed s := infClosure.isClosed_iff.symm
Characterization of Inf-closed Sets via Inf-closure
Informal description
For any subset $s$ of a meet-semilattice, the inf-closure of $s$ equals $s$ if and only if $s$ is inf-closed. In other words, $\text{infClosure}(s) = s \leftrightarrow \text{InfClosed}(s)$.
infClosure_idem theorem
(s : Set α) : infClosure (infClosure s) = infClosure s
Full source 
lemma infClosure_idem (s : Set α) : infClosure (infClosure s) = infClosure s :=
  infClosure.idempotent _
Idempotence of Inf-closure
Informal description
For any subset $s$ of a meet-semilattice $\alpha$, the inf-closure of the inf-closure of $s$ is equal to the inf-closure of $s$, i.e., $\text{infClosure}(\text{infClosure}(s)) = \text{infClosure}(s)$.
infClosure_empty theorem
: infClosure (∅ : Set α) = ∅
Full source 
@[simp] lemma infClosure_empty : infClosure (∅ : Set α) = ∅ := by simp
Inf-closure of Empty Set is Empty
Informal description
The inf-closure of the empty set in a meet-semilattice $\alpha$ is the empty set itself, i.e., $\text{infClosure}(\emptyset) = \emptyset$.
infClosure_singleton theorem
: infClosure { a } = { a }
Full source 
@[simp] lemma infClosure_singleton : infClosure {a} = {a} := by simp
Inf-closure of a singleton set is itself
Informal description
For any element $a$ in a meet-semilattice $\alpha$, the inf-closure of the singleton set $\{a\}$ is $\{a\}$ itself, i.e., $\text{infClosure}(\{a\}) = \{a\}$.
infClosure_univ theorem
: infClosure (Set.univ : Set α) = Set.univ
Full source 
@[simp] lemma infClosure_univ : infClosure (Set.univ : Set α) = Set.univ := by simp
Inf-closure of universal set is universal
Informal description
The inf-closure of the universal set $\text{univ}$ in a meet-semilattice is equal to $\text{univ}$ itself.
lowerBounds_infClosure theorem
(s : Set α) : lowerBounds (infClosure s) = lowerBounds s
Full source 
@[simp] lemma lowerBounds_infClosure (s : Set α) : lowerBounds (infClosure s) = lowerBounds s :=
  (lowerBounds_mono_set subset_infClosure).antisymm <| by
    rintro a ha _ ⟨t, ht, hts, rfl⟩
    exact le_inf' _ _ fun b hb ↦ ha <| hts hb
Lower Bounds of Inf-closure Equal Lower Bounds of Original Set
Informal description
For any set $s$ in a meet-semilattice, the set of lower bounds of the inf-closure of $s$ is equal to the set of lower bounds of $s$, i.e., $\text{lowerBounds}(\text{infClosure}(s)) = \text{lowerBounds}(s)$.
isGLB_infClosure theorem
: IsGLB (infClosure s) a ↔ IsGLB s a
Full source 
@[simp] lemma isGLB_infClosure : IsGLBIsGLB (infClosure s) a ↔ IsGLB s a := by simp [IsGLB]
Greatest Lower Bound Characterization for Inf-closure: $\text{IsGLB}(\text{infClosure}(s), a) \leftrightarrow \text{IsGLB}(s, a)$
Informal description
An element $a$ is the greatest lower bound of the inf-closure of a set $s$ if and only if $a$ is the greatest lower bound of $s$ itself. In other words, $\text{IsGLB}(\text{infClosure}(s), a) \leftrightarrow \text{IsGLB}(s, a)$.
finsetInf'_mem_infClosure theorem
{ι : Type*} {t : Finset ι} (ht : t.Nonempty) {f : ι → α} (hf : ∀ i ∈ t, f i ∈ s) : t.inf' ht f ∈ infClosure s
Full source 
lemma finsetInf'_mem_infClosure {ι : Type*} {t : Finset ι} (ht : t.Nonempty) {f : ι → α}
    (hf : ∀ i ∈ t, f i ∈ s) : t.inf' ht f ∈ infClosure s :=
  infClosed_infClosure.finsetInf'_mem _ fun _i hi ↦ subset_infClosure <| hf _ hi
Infimum of Finite Family in Set Belongs to Inf-Closure
Informal description
Let $s$ be a set in a meet-semilattice, and let $t$ be a nonempty finite set indexed by type $\iota$. If for every $i \in t$, the element $f(i)$ belongs to $s$, then the infimum of the family $\{f(i)\}_{i \in t}$ (denoted as $\bigsqcap_{i \in t} f(i)$) belongs to the inf-closure of $s$.
Set.Finite.infClosure theorem
(hs : s.Finite) : (infClosure s).Finite
Full source 
/-- The semilatice generated by a finite set is finite. -/
protected lemma Set.Finite.infClosure (hs : s.Finite) : (infClosure s).Finite := by
  lift s to Finset α using hs
  classical
  refine ({t ∈ s.powerset | t.Nonempty}.attach.image
    fun t ↦ t.1.inf' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_
  rintro _ ⟨t, ht, hts, rfl⟩
  simp only [id_eq, coe_image, mem_image, mem_coe, mem_attach, true_and, Subtype.exists,
    Finset.mem_powerset, Finset.not_nonempty_iff_eq_empty, mem_filter]
  exact ⟨t, ⟨hts, ht⟩, rfl⟩
Finiteness of Inf-closure for Finite Sets
Informal description
For any finite subset $s$ of a meet-semilattice, the inf-closure of $s$ is also finite.
infClosure_prod theorem
(s : Set α) (t : Set β) : infClosure (s ×ˢ t) = infClosure s ×ˢ infClosure t
Full source 
@[simp] lemma infClosure_prod (s : Set α) (t : Set β) :
    infClosure (s ×ˢ t) = infClosure s ×ˢ infClosure t :=
  le_antisymm (infClosure_min (Set.prod_mono subset_infClosure subset_infClosure) <|
    infClosed_infClosure.prod infClosed_infClosure) <| by
      rintro ⟨_, _⟩ ⟨⟨u, hu, hus, rfl⟩, v, hv, hvt, rfl⟩
      refine ⟨u ×ˢ v, hu.product hv, ?_, ?_⟩
      · simpa only [coe_product] using Set.prod_mono hus hvt
      · simp [prodMk_inf'_inf']
Inf-closure of Cartesian Product Equals Product of Inf-closures
Informal description
For any sets $s$ in a meet-semilattice $\alpha$ and $t$ in a meet-semilattice $\beta$, the inf-closure of their Cartesian product $s \times t$ is equal to the Cartesian product of their inf-closures, i.e., \[ \text{infClosure}(s \times t) = \text{infClosure}(s) \times \text{infClosure}(t). \]
latticeClosure definition
: ClosureOperator (Set α)
Full source 
/-- Every set in a join-semilattice generates a set closed under join. -/
@[simps! isClosed]
def latticeClosure : ClosureOperator (Set α) :=
  .ofCompletePred IsSublattice fun _ ↦ isSublattice_sInter
Lattice closure of a set
Informal description
The `latticeClosure` operator maps a subset $s$ of a lattice $\alpha$ to the smallest sublattice containing $s$. Here, a sublattice is a subset closed under both join ($\sqcup$) and meet ($\sqcap$).
subset_latticeClosure theorem
: s ⊆ latticeClosure s
Full source 
@[simp] lemma subset_latticeClosure : s ⊆ latticeClosure s := latticeClosure.le_closure _
Subset Property of Lattice Closure
Informal description
For any subset $s$ of a lattice $\alpha$, the set $s$ is contained in its lattice closure, i.e., $s \subseteq \text{latticeClosure}(s)$.
latticeClosure_mono theorem
: Monotone (latticeClosure : Set α → Set α)
Full source 
lemma latticeClosure_mono : Monotone (latticeClosure : Set α → Set α) := latticeClosure.monotone
Monotonicity of Lattice Closure
Informal description
The lattice closure operator is monotone, meaning that for any subsets $s$ and $t$ of a lattice $\alpha$, if $s \subseteq t$, then the lattice closure of $s$ is contained in the lattice closure of $t$.
latticeClosure_idem theorem
(s : Set α) : latticeClosure (latticeClosure s) = latticeClosure s
Full source 
lemma latticeClosure_idem (s : Set α) : latticeClosure (latticeClosure s) = latticeClosure s :=
  latticeClosure.idempotent _
Idempotence of Lattice Closure Operator
Informal description
For any subset $s$ of a lattice $\alpha$, applying the lattice closure operator twice is equivalent to applying it once, i.e., $\text{latticeClosure}(\text{latticeClosure}(s)) = \text{latticeClosure}(s)$.
latticeClosure_empty theorem
: latticeClosure (∅ : Set α) = ∅
Full source 
@[simp] lemma latticeClosure_empty : latticeClosure (∅ : Set α) = ∅ := by simp
Lattice Closure of Empty Set is Empty
Informal description
The lattice closure of the empty set in a lattice $\alpha$ is the empty set itself, i.e., $\text{latticeClosure}(\emptyset) = \emptyset$.
latticeClosure_singleton theorem
(a : α) : latticeClosure { a } = { a }
Full source 
@[simp] lemma latticeClosure_singleton (a : α) : latticeClosure {a} = {a} := by simp
Lattice Closure of Singleton is Singleton
Informal description
For any element $a$ in a lattice $\alpha$, the smallest sublattice containing the singleton set $\{a\}$ is $\{a\}$ itself. That is, $\text{latticeClosure}(\{a\}) = \{a\}$.
latticeClosure_univ theorem
: latticeClosure (Set.univ : Set α) = Set.univ
Full source 
@[simp] lemma latticeClosure_univ : latticeClosure (Set.univ : Set α) = Set.univ := by simp
Lattice Closure of Universal Set is Universal Set
Informal description
The lattice closure of the universal set in a lattice $\alpha$ is the universal set itself. In other words, if $s$ is the entire set $\alpha$, then the smallest sublattice containing $s$ is $\alpha$.
SupClosed.infClosure theorem
(hs : SupClosed s) : SupClosed (infClosure s)
Full source 
protected lemma SupClosed.infClosure (hs : SupClosed s) : SupClosed (infClosure s) := by
  rintro _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩
  rw [inf'_sup_inf']
  exact finsetInf'_mem_infClosure _
    fun i hi ↦ hs (hts (mem_product.1 hi).1) (hus (mem_product.1 hi).2)
Sup-closed sets have sup-closed inf-closures
Informal description
If a set $s$ in a join-semilattice is sup-closed (i.e., closed under the join operation $\sqcup$), then its inf-closure (the smallest inf-closed set containing $s$) is also sup-closed.
InfClosed.supClosure theorem
(hs : InfClosed s) : InfClosed (supClosure s)
Full source 
protected lemma InfClosed.supClosure (hs : InfClosed s) : InfClosed (supClosure s) := by
  rintro _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩
  rw [sup'_inf_sup']
  exact finsetSup'_mem_supClosure _
    fun i hi ↦ hs (hts (mem_product.1 hi).1) (hus (mem_product.1 hi).2)
Inf-closed sets have inf-closed sup-closures
Informal description
If a set $s$ in a meet-semilattice is inf-closed (i.e., closed under the meet operation $\sqcap$), then its sup-closure (the smallest sup-closed set containing $s$) is also inf-closed.
supClosure_infClosure theorem
(s : Set α) : supClosure (infClosure s) = latticeClosure s
Full source 
@[simp] lemma supClosure_infClosure (s : Set α) : supClosure (infClosure s) = latticeClosure s :=
  le_antisymm (supClosure_min (infClosure_min subset_latticeClosure isSublattice_latticeClosure.2)
    isSublattice_latticeClosure.1) <| latticeClosure_min (subset_infClosure.trans subset_supClosure)
      ⟨supClosed_supClosure, infClosed_infClosure.supClosure⟩
Sup-closure of Inf-closure Equals Lattice Closure
Informal description
For any subset $s$ of a lattice $\alpha$, the sup-closure of the inf-closure of $s$ is equal to the lattice closure of $s$, i.e., $\text{supClosure}(\text{infClosure}(s)) = \text{latticeClosure}(s)$.
infClosure_supClosure theorem
(s : Set α) : infClosure (supClosure s) = latticeClosure s
Full source 
@[simp] lemma infClosure_supClosure (s : Set α) : infClosure (supClosure s) = latticeClosure s :=
  le_antisymm (infClosure_min (supClosure_min subset_latticeClosure isSublattice_latticeClosure.1)
    isSublattice_latticeClosure.2) <| latticeClosure_min (subset_supClosure.trans subset_infClosure)
      ⟨supClosed_supClosure.infClosure, infClosed_infClosure⟩
Inf-closure of Sup-closure Equals Lattice Closure
Informal description
For any subset $s$ of a lattice $\alpha$, the inf-closure of the sup-closure of $s$ is equal to the lattice closure of $s$, i.e., \[ \text{infClosure}(\text{supClosure}(s)) = \text{latticeClosure}(s). \]
latticeClosure_prod theorem
(s : Set α) (t : Set β) : latticeClosure (s ×ˢ t) = latticeClosure s ×ˢ latticeClosure t
Full source 
@[simp] lemma latticeClosure_prod (s : Set α) (t : Set β) :
    latticeClosure (s ×ˢ t) = latticeClosure s ×ˢ latticeClosure t := by
  simp_rw [← supClosure_infClosure]; simp
Lattice Closure of Cartesian Product Equals Product of Lattice Closures
Informal description
For any subsets $s$ of a lattice $\alpha$ and $t$ of a lattice $\beta$, the lattice closure of their Cartesian product $s \times t$ is equal to the Cartesian product of their individual lattice closures, i.e., \[ \text{latticeClosure}(s \times t) = \text{latticeClosure}(s) \times \text{latticeClosure}(t). \]
SemilatticeSup.toCompleteSemilatticeSup definition
[SemilatticeSup α] (sSup : Set α → α) (h : ∀ s, SupClosed s → IsLUB s (sSup s)) : CompleteSemilatticeSup α
Full source 
/-- A join-semilattice where every sup-closed set has a least upper bound is automatically complete.
-/
def SemilatticeSup.toCompleteSemilatticeSup [SemilatticeSup α] (sSup : Set α → α)
    (h : ∀ s, SupClosed s → IsLUB s (sSup s)) : CompleteSemilatticeSup α where
  sSup := fun s => sSup (supClosure s)
  le_sSup _ _ ha := (h _ supClosed_supClosure).1 <| subset_supClosure ha
  sSup_le s a ha := (isLUB_le_iff <| h _ supClosed_supClosure).2 <| by rwa [upperBounds_supClosure]
Completion of a join-semilattice via sup-closed sets
Informal description
Given a join-semilattice $\alpha$ and a function $\mathrm{sSup} : \mathrm{Set} \ \alpha \to \alpha$ such that for every sup-closed set $s \subseteq \alpha$, $\mathrm{sSup} \ s$ is the least upper bound of $s$, then $\alpha$ is automatically a complete join-semilattice. Here, the supremum of any set $s$ is defined as $\mathrm{sSup}$ applied to the sup-closure of $s$.
SemilatticeInf.toCompleteSemilatticeInf definition
[SemilatticeInf α] (sInf : Set α → α) (h : ∀ s, InfClosed s → IsGLB s (sInf s)) : CompleteSemilatticeInf α
Full source 
/-- A meet-semilattice where every inf-closed set has a greatest lower bound is automatically
complete. -/
def SemilatticeInf.toCompleteSemilatticeInf [SemilatticeInf α] (sInf : Set α → α)
    (h : ∀ s, InfClosed s → IsGLB s (sInf s)) : CompleteSemilatticeInf α where
  sInf := fun s => sInf (infClosure s)
  sInf_le _ _ ha := (h _ infClosed_infClosure).1 <| subset_infClosure ha
  le_sInf s a ha := (le_isGLB_iff <| h _ infClosed_infClosure).2 <| by rwa [lowerBounds_infClosure]
Completion of a meet-semilattice via inf-closed sets
Informal description
Given a meet-semilattice $\alpha$ and a function $\mathrm{sInf} : \mathrm{Set} \ \alpha \to \alpha$ such that for every inf-closed set $s \subseteq \alpha$, $\mathrm{sInf} \ s$ is the greatest lower bound of $s$, then $\alpha$ is automatically a complete meet-semilattice. Here, the infimum of any set $s$ is defined as $\mathrm{sInf}$ applied to the inf-closure of $s$.
SupClosed.iSup_mem_of_nonempty theorem
[Finite ι] [Nonempty ι] (hs : SupClosed s) (hf : ∀ i, f i ∈ s) : ⨆ i, f i ∈ s
Full source 
lemma SupClosed.iSup_mem_of_nonempty [Finite ι] [Nonempty ι] (hs : SupClosed s)
    (hf : ∀ i, f i ∈ s) : ⨆ i, f i⨆ i, f i ∈ s := by
  cases nonempty_fintype (PLift ι)
  rw [← iSup_plift_down, ← Finset.sup'_univ_eq_ciSup]
  exact hs.finsetSup'_mem Finset.univ_nonempty fun _ _ ↦ hf _
Sup-closed sets are closed under finite nonempty indexed joins
Informal description
Let $\alpha$ be a type with a join operation $\sqcup$, and let $s$ be a sup-closed subset of $\alpha$. For any finite nonempty type $\iota$ and any function $f : \iota \to \alpha$ such that $f(i) \in s$ for all $i \in \iota$, the indexed supremum $\bigsqcup_{i \in \iota} f(i)$ is also in $s$.
InfClosed.iInf_mem_of_nonempty theorem
[Finite ι] [Nonempty ι] (hs : InfClosed s) (hf : ∀ i, f i ∈ s) : ⨅ i, f i ∈ s
Full source 
lemma InfClosed.iInf_mem_of_nonempty [Finite ι] [Nonempty ι] (hs : InfClosed s)
    (hf : ∀ i, f i ∈ s) : ⨅ i, f i⨅ i, f i ∈ s := hs.dual.iSup_mem_of_nonempty hf
Inf-closed sets are closed under finite nonempty indexed meets
Informal description
Let $\alpha$ be a type with a meet operation $\sqcap$, and let $s \subseteq \alpha$ be an inf-closed subset. For any finite nonempty type $\iota$ and any function $f : \iota \to \alpha$ such that $f(i) \in s$ for all $i \in \iota$, the indexed infimum $\bigsqcap_{i \in \iota} f(i)$ is also in $s$.
SupClosed.sSup_mem_of_nonempty theorem
(hs : SupClosed s) (ht : t.Finite) (ht' : t.Nonempty) (hts : t ⊆ s) : sSup t ∈ s
Full source 
lemma SupClosed.sSup_mem_of_nonempty (hs : SupClosed s) (ht : t.Finite) (ht' : t.Nonempty)
    (hts : t ⊆ s) : sSupsSup t ∈ s := by
  have := ht.to_subtype
  have := ht'.to_subtype
  rw [sSup_eq_iSup']
  exact hs.iSup_mem_of_nonempty (by simpa)
Supremum of Finite Nonempty Subset in Sup-closed Set
Informal description
Let $s$ be a sup-closed subset of a type $\alpha$ with a join operation $\sqcup$, and let $t$ be a finite nonempty subset of $s$. Then the supremum $\sup t$ is also in $s$.
InfClosed.sInf_mem_of_nonempty theorem
(hs : InfClosed s) (ht : t.Finite) (ht' : t.Nonempty) (hts : t ⊆ s) : sInf t ∈ s
Full source 
lemma InfClosed.sInf_mem_of_nonempty (hs : InfClosed s) (ht : t.Finite) (ht' : t.Nonempty)
    (hts : t ⊆ s) : sInfsInf t ∈ s := hs.dual.sSup_mem_of_nonempty ht ht' hts
Infimum of Finite Nonempty Subset in Inf-closed Set
Informal description
Let $s$ be an inf-closed subset of a type $\alpha$ with a meet operation $\sqcap$, and let $t$ be a finite nonempty subset of $s$. Then the infimum $\inf t$ is also in $s$.
SupClosed.biSup_mem_of_nonempty theorem
{ι : Type*} {t : Set ι} {f : ι → α} (hs : SupClosed s) (ht : t.Finite) (ht' : t.Nonempty) (hf : ∀ i ∈ t, f i ∈ s) : ⨆ i ∈ t, f i ∈ s
Full source 
lemma SupClosed.biSup_mem_of_nonempty {ι : Type*} {t : Set ι} {f : ι → α} (hs : SupClosed s)
    (ht : t.Finite) (ht' : t.Nonempty) (hf : ∀ i ∈ t, f i ∈ s) : ⨆ i ∈ t, f i⨆ i ∈ t, f i ∈ s := by
  rw [← sSup_image]
  exact hs.sSup_mem_of_nonempty (ht.image _) (by simpa) (by simpa)
Bounded Supremum of Finite Nonempty Indexed Family in Sup-closed Set
Informal description
Let $\alpha$ be a type with a join operation $\sqcup$, and let $s$ be a sup-closed subset of $\alpha$. For any finite nonempty subset $t$ of an index type $\iota$ and any function $f : \iota \to \alpha$ such that $f(i) \in s$ for all $i \in t$, the bounded supremum $\bigsqcup_{i \in t} f(i)$ is also in $s$.
InfClosed.biInf_mem_of_nonempty theorem
{ι : Type*} {t : Set ι} {f : ι → α} (hs : InfClosed s) (ht : t.Finite) (ht' : t.Nonempty) (hf : ∀ i ∈ t, f i ∈ s) : ⨅ i ∈ t, f i ∈ s
Full source 
lemma InfClosed.biInf_mem_of_nonempty {ι : Type*} {t : Set ι} {f : ι → α} (hs : InfClosed s)
    (ht : t.Finite) (ht' : t.Nonempty) (hf : ∀ i ∈ t, f i ∈ s) : ⨅ i ∈ t, f i⨅ i ∈ t, f i ∈ s :=
  hs.dual.biSup_mem_of_nonempty ht ht' hf
Bounded Infimum of Finite Nonempty Indexed Family in Inf-closed Set
Informal description
Let $\alpha$ be a type with a meet operation $\sqcap$, and let $s$ be an inf-closed subset of $\alpha$. For any finite nonempty subset $t$ of an index type $\iota$ and any function $f : \iota \to \alpha$ such that $f(i) \in s$ for all $i \in t$, the bounded infimum $\bigsqcap_{i \in t} f(i)$ is also in $s$.
SupClosed.iSup_mem theorem
[Finite ι] (hs : SupClosed s) (hbot : ⊥ ∈ s) (hf : ∀ i, f i ∈ s) : ⨆ i, f i ∈ s
Full source 
lemma SupClosed.iSup_mem [Finite ι] (hs : SupClosed s) (hbot : ⊥⊥ ∈ s) (hf : ∀ i, f i ∈ s) :
    ⨆ i, f i⨆ i, f i ∈ s := by
  cases isEmpty_or_nonempty ι
  · simpa [iSup_of_empty]
  · exact hs.iSup_mem_of_nonempty hf
Sup-closed sets containing bottom are closed under finite indexed joins
Informal description
Let $\alpha$ be a type with a join operation $\sqcup$ and a bottom element $\bot$, and let $s$ be a sup-closed subset of $\alpha$ containing $\bot$. For any finite type $\iota$ and any function $f : \iota \to \alpha$ such that $f(i) \in s$ for all $i \in \iota$, the indexed supremum $\bigsqcup_{i \in \iota} f(i)$ is also in $s$.
InfClosed.iInf_mem theorem
[Finite ι] (hs : InfClosed s) (htop : ⊤ ∈ s) (hf : ∀ i, f i ∈ s) : ⨅ i, f i ∈ s
Full source 
lemma InfClosed.iInf_mem [Finite ι] (hs : InfClosed s) (htop : ⊤⊤ ∈ s) (hf : ∀ i, f i ∈ s) :
    ⨅ i, f i⨅ i, f i ∈ s := hs.dual.iSup_mem htop hf
Inf-closed sets containing top are closed under finite indexed meets
Informal description
Let $\alpha$ be a type with a meet operation $\sqcap$ and a top element $\top$, and let $s$ be an inf-closed subset of $\alpha$ containing $\top$. For any finite type $\iota$ and any function $f : \iota \to \alpha$ such that $f(i) \in s$ for all $i \in \iota$, the indexed infimum $\bigsqcap_{i \in \iota} f(i)$ is also in $s$.
SupClosed.sSup_mem theorem
(hs : SupClosed s) (ht : t.Finite) (hbot : ⊥ ∈ s) (hts : t ⊆ s) : sSup t ∈ s
Full source 
lemma SupClosed.sSup_mem (hs : SupClosed s) (ht : t.Finite) (hbot : ⊥⊥ ∈ s) (hts : t ⊆ s) :
    sSupsSup t ∈ s := by
  have := ht.to_subtype
  rw [sSup_eq_iSup']
  exact hs.iSup_mem hbot (by simpa)
Supremum of Finite Subset in Sup-closed Set
Informal description
Let $s$ be a sup-closed subset of a type $\alpha$ with a join operation $\sqcup$ and a bottom element $\bot$. For any finite subset $t \subseteq s$ containing $\bot$, the supremum $\bigsqcup t$ is also in $s$.
InfClosed.sInf_mem theorem
(hs : InfClosed s) (ht : t.Finite) (htop : ⊤ ∈ s) (hts : t ⊆ s) : sInf t ∈ s
Full source 
lemma InfClosed.sInf_mem (hs : InfClosed s) (ht : t.Finite) (htop : ⊤⊤ ∈ s) (hts : t ⊆ s) :
    sInfsInf t ∈ s := hs.dual.sSup_mem ht htop hts
Infimum of Finite Subset in Inf-closed Set
Informal description
Let $s$ be an inf-closed subset of a type $\alpha$ with a meet operation $\sqcap$ and a top element $\top$. For any finite subset $t \subseteq s$ containing $\top$, the infimum $\bigsqcap t$ is also in $s$.
SupClosed.biSup_mem theorem
{ι : Type*} {t : Set ι} {f : ι → α} (hs : SupClosed s) (ht : t.Finite) (hbot : ⊥ ∈ s) (hf : ∀ i ∈ t, f i ∈ s) : ⨆ i ∈ t, f i ∈ s
Full source 
lemma SupClosed.biSup_mem {ι : Type*} {t : Set ι} {f : ι → α} (hs : SupClosed s)
    (ht : t.Finite) (hbot : ⊥⊥ ∈ s) (hf : ∀ i ∈ t, f i ∈ s) : ⨆ i ∈ t, f i⨆ i ∈ t, f i ∈ s := by
  rw [← sSup_image]
  exact hs.sSup_mem (ht.image _) hbot (by simpa)
Supremum of Finite Indexed Family in Sup-closed Set
Informal description
Let $s$ be a sup-closed subset of a type $\alpha$ with a join operation $\sqcup$ and a bottom element $\bot$. For any finite set $t \subseteq \iota$ and any function $f : \iota \to \alpha$ such that $f(i) \in s$ for all $i \in t$, the supremum $\bigsqcup_{i \in t} f(i)$ is also in $s$.
InfClosed.biInf_mem theorem
{ι : Type*} {t : Set ι} {f : ι → α} (hs : InfClosed s) (ht : t.Finite) (htop : ⊤ ∈ s) (hf : ∀ i ∈ t, f i ∈ s) : ⨅ i ∈ t, f i ∈ s
Full source 
lemma InfClosed.biInf_mem {ι : Type*} {t : Set ι} {f : ι → α} (hs : InfClosed s)
    (ht : t.Finite) (htop : ⊤⊤ ∈ s) (hf : ∀ i ∈ t, f i ∈ s) : ⨅ i ∈ t, f i⨅ i ∈ t, f i ∈ s :=
  hs.dual.biSup_mem ht htop hf
Infimum of Finite Indexed Family in Inf-closed Set
Informal description
Let $\alpha$ be a type with a meet operation $\sqcap$ and a top element $\top$. Given an inf-closed subset $s \subseteq \alpha$, a finite set $t \subseteq \iota$, and a function $f : \iota \to \alpha$ such that $f(i) \in s$ for all $i \in t$, the infimum $\bigsqcap_{i \in t} f(i)$ is also in $s$.