doc-next-gen

Mathlib.Order.UpperLower.Closure

Module docstring

{"# Upper and lower closures

Upper (lower) closures generalise principal upper (lower) sets to arbitrary included sets. Indeed, they are equivalent to a union over principal upper (lower) sets, as shown in coe_upperClosure (coe_lowerClosure).

Main declarations

  • upperClosure: The greatest upper set containing a set.
  • lowerClosure: The least lower set containing a set. ","### Set Difference "}
upperClosure definition
(s : Set α) : UpperSet α
Full source 
/-- The greatest upper set containing a given set. -/
def upperClosure (s : Set α) : UpperSet α :=
  ⟨{ x | ∃ a ∈ s, a ≤ x }, fun _ _ hle h => h.imp fun _x hx => ⟨hx.1, hx.2.trans hle⟩⟩
Upper closure of a set
Informal description
For a set $s$ in a partially ordered type $\alpha$, the upper closure of $s$ is the set of all elements $x$ in $\alpha$ such that there exists an element $a$ in $s$ with $a \leq x$. It is the smallest upper set containing $s$.
lowerClosure definition
(s : Set α) : LowerSet α
Full source 
/-- The least lower set containing a given set. -/
def lowerClosure (s : Set α) : LowerSet α :=
  ⟨{ x | ∃ a ∈ s, x ≤ a }, fun _ _ hle h => h.imp fun _x hx => ⟨hx.1, hle.trans hx.2⟩⟩
Lower closure of a set
Informal description
Given a set \( s \) in a partially ordered set \( \alpha \), the lower closure of \( s \) is the smallest lower set containing \( s \). It consists of all elements \( x \in \alpha \) such that there exists an element \( a \in s \) with \( x \leq a \).
coe_upperClosure theorem
(s : Set α) : ↑(upperClosure s) = ⋃ a ∈ s, Ici a
Full source 
@[norm_cast]
theorem coe_upperClosure (s : Set α) : ↑(upperClosure s) = ⋃ a ∈ s, Ici a := by
  ext
  simp
Characterization of Upper Closure as Union of Principal Upper Sets
Informal description
For any set $s$ in a preorder $\alpha$, the carrier set of the upper closure of $s$ is equal to the union of all left-closed right-infinite intervals $[a, \infty)$ where $a$ ranges over $s$. In other words, $\text{upperClosure}(s) = \bigcup_{a \in s} [a, \infty)$.
coe_lowerClosure theorem
(s : Set α) : ↑(lowerClosure s) = ⋃ a ∈ s, Iic a
Full source 
@[norm_cast]
theorem coe_lowerClosure (s : Set α) : ↑(lowerClosure s) = ⋃ a ∈ s, Iic a := by
  ext
  simp
Characterization of Lower Closure as Union of Principal Lower Sets
Informal description
For any set $s$ in a preorder $\alpha$, the underlying set of the lower closure of $s$ is equal to the union of all left-infinite right-closed intervals $(-\infty, a]$ for $a \in s$. That is, \[ \text{lowerClosure}(s) = \bigcup_{a \in s} (-\infty, a]. \]
instDecidablePredMemUpperClosure instance
[DecidablePred (∃ a ∈ s, a ≤ ·)] : DecidablePred (· ∈ upperClosure s)
Full source 
instance instDecidablePredMemUpperClosure [DecidablePred (∃ a ∈ s, a ≤ ·)] :
    DecidablePred (· ∈ upperClosure s) := ‹DecidablePred _›
Decidability of Membership in Upper Closure
Informal description
For any set $s$ in a partially ordered type $\alpha$, if there exists a decidable predicate for the existence of an element $a \in s$ such that $a \leq \cdot$, then membership in the upper closure of $s$ is decidable.
instDecidablePredMemLowerClosure instance
[DecidablePred (∃ a ∈ s, · ≤ a)] : DecidablePred (· ∈ lowerClosure s)
Full source 
instance instDecidablePredMemLowerClosure [DecidablePred (∃ a ∈ s, · ≤ a)] :
    DecidablePred (· ∈ lowerClosure s) := ‹DecidablePred _›
Decidability of Membership in Lower Closure
Informal description
For any set $s$ in a partially ordered set $\alpha$, if there exists a decidable predicate for the existence of an element $a \in s$ such that $x \leq a$ for any $x \in \alpha$, then membership in the lower closure of $s$ is decidable.
subset_upperClosure theorem
: s ⊆ upperClosure s
Full source 
theorem subset_upperClosure : s ⊆ upperClosure s := fun x hx => ⟨x, hx, le_rfl⟩
Inclusion of Set in its Upper Closure
Informal description
For any subset $s$ of a partially ordered set $\alpha$, the set $s$ is contained in its upper closure, i.e., $s \subseteq \text{upperClosure}(s)$.
subset_lowerClosure theorem
: s ⊆ lowerClosure s
Full source 
theorem subset_lowerClosure : s ⊆ lowerClosure s := fun x hx => ⟨x, hx, le_rfl⟩
Inclusion of Set in its Lower Closure
Informal description
For any subset $s$ of a partially ordered set, $s$ is contained in its lower closure, i.e., $s \subseteq \text{lowerClosure}(s)$.
upperClosure_min theorem
(h : s ⊆ t) (ht : IsUpperSet t) : ↑(upperClosure s) ⊆ t
Full source 
theorem upperClosure_min (h : s ⊆ t) (ht : IsUpperSet t) : ↑(upperClosure s) ⊆ t :=
  fun _a ⟨_b, hb, hba⟩ => ht hba <| h hb
Minimality Property of Upper Closure
Informal description
For any sets $s$ and $t$ in a partially ordered set, if $s \subseteq t$ and $t$ is an upper set, then the upper closure of $s$ is contained in $t$.
lowerClosure_min theorem
(h : s ⊆ t) (ht : IsLowerSet t) : ↑(lowerClosure s) ⊆ t
Full source 
theorem lowerClosure_min (h : s ⊆ t) (ht : IsLowerSet t) : ↑(lowerClosure s) ⊆ t :=
  fun _a ⟨_b, hb, hab⟩ => ht hab <| h hb
Minimality Property of Lower Closure
Informal description
For any sets $s$ and $t$ in a partially ordered set, if $s \subseteq t$ and $t$ is a lower set, then the lower closure of $s$ is contained in $t$.
IsUpperSet.upperClosure theorem
(hs : IsUpperSet s) : ↑(upperClosure s) = s
Full source 
protected theorem IsUpperSet.upperClosure (hs : IsUpperSet s) : ↑(upperClosure s) = s :=
  (upperClosure_min Subset.rfl hs).antisymm subset_upperClosure
Upper Closure of an Upper Set is Itself
Informal description
For any subset $s$ of a partially ordered set $\alpha$, if $s$ is an upper set (i.e., for all $x \in s$ and $y \geq x$, $y \in s$), then the upper closure of $s$ is equal to $s$ itself, i.e., $\text{upperClosure}(s) = s$.
UpperSet.upperClosure theorem
(s : UpperSet α) : upperClosure (s : Set α) = s
Full source 
@[simp]
protected theorem UpperSet.upperClosure (s : UpperSet α) : upperClosure (s : Set α) = s :=
  SetLike.coe_injective s.2.upperClosure
Upper Closure of an Upper Set is Itself
Informal description
For any upper set $s$ in a partially ordered type $\alpha$, the upper closure of the underlying set of $s$ is equal to $s$ itself, i.e., $\text{upperClosure}(s) = s$.
LowerSet.lowerClosure theorem
(s : LowerSet α) : lowerClosure (s : Set α) = s
Full source 
@[simp]
protected theorem LowerSet.lowerClosure (s : LowerSet α) : lowerClosure (s : Set α) = s :=
  SetLike.coe_injective s.2.lowerClosure
Lower Closure of a Lower Set is Itself
Informal description
For any lower set $s$ in a partially ordered type $\alpha$, the lower closure of the underlying set of $s$ is equal to $s$ itself, i.e., $\text{lowerClosure}(s) = s$.
upperClosure_image theorem
(f : α ≃o β) : upperClosure (f '' s) = UpperSet.map f (upperClosure s)
Full source 
@[simp]
theorem upperClosure_image (f : α ≃o β) :
    upperClosure (f '' s) = UpperSet.map f (upperClosure s) := by
  rw [← f.symm_symm, ← UpperSet.symm_map, f.symm_symm]
  ext
  simp [-UpperSet.symm_map, UpperSet.map, OrderIso.symm, ← f.le_symm_apply]
Upper Closure Commutes with Order Isomorphism Image
Informal description
Let $\alpha$ and $\beta$ be preordered sets and $f : \alpha \simeq \beta$ be an order isomorphism. For any subset $s \subseteq \alpha$, the upper closure of the image $f(s)$ in $\beta$ equals the image under $f$ of the upper closure of $s$ in $\alpha$. That is, $$\text{upperClosure}(f(s)) = f(\text{upperClosure}(s)).$$
lowerClosure_image theorem
(f : α ≃o β) : lowerClosure (f '' s) = LowerSet.map f (lowerClosure s)
Full source 
@[simp]
theorem lowerClosure_image (f : α ≃o β) :
    lowerClosure (f '' s) = LowerSet.map f (lowerClosure s) := by
  rw [← f.symm_symm, ← LowerSet.symm_map, f.symm_symm]
  ext
  simp [-LowerSet.symm_map, LowerSet.map, OrderIso.symm, ← f.symm_apply_le]
Lower Closure of Image under Order Isomorphism Equals Image of Lower Closure
Informal description
Given an order isomorphism $f : \alpha \simeq \beta$ between preordered sets $\alpha$ and $\beta$, and a subset $s \subseteq \alpha$, the lower closure of the image $f(s)$ in $\beta$ is equal to the image of the lower closure of $s$ under the induced map on lower sets. That is, $$\text{lowerClosure}(f(s)) = f(\text{lowerClosure}(s))$$ where $\text{lowerClosure}(s)$ denotes the smallest lower set containing $s$.
UpperSet.iInf_Ici theorem
(s : Set α) : ⨅ a ∈ s, UpperSet.Ici a = upperClosure s
Full source 
@[simp]
theorem UpperSet.iInf_Ici (s : Set α) : ⨅ a ∈ s, UpperSet.Ici a = upperClosure s := by
  ext
  simp
Infimum of Principal Upper Sets Equals Upper Closure
Informal description
For any subset $s$ of a preordered set $\alpha$, the infimum of the family of principal upper sets $\text{Ici}(a)$ for $a \in s$ is equal to the upper closure of $s$. That is, $$ \bigsqcap_{a \in s} [a, \infty) = \text{upperClosure}(s) $$ where $\text{upperClosure}(s)$ is the smallest upper set containing $s$.
LowerSet.iSup_Iic theorem
(s : Set α) : ⨆ a ∈ s, LowerSet.Iic a = lowerClosure s
Full source 
@[simp]
theorem LowerSet.iSup_Iic (s : Set α) : ⨆ a ∈ s, LowerSet.Iic a = lowerClosure s := by
  ext
  simp
Supremum of Principal Lower Sets Equals Lower Closure
Informal description
For any subset $s$ of a preordered set $\alpha$, the supremum of the family of principal lower sets $\text{Iic}(a)$ for $a \in s$ is equal to the lower closure of $s$. That is, $$ \bigsqcup_{a \in s} (-\infty, a] = \text{lowerClosure}(s) $$ where $\text{lowerClosure}(s)$ is the smallest lower set containing $s$.
lowerClosure_le theorem
{t : LowerSet α} : lowerClosure s ≤ t ↔ s ⊆ t
Full source 
@[simp] lemma lowerClosure_le {t : LowerSet α} : lowerClosurelowerClosure s ≤ t ↔ s ⊆ t :=
  ⟨fun h ↦ subset_lowerClosure.trans <| LowerSet.coe_subset_coe.2 h,
    fun h ↦ lowerClosure_min h t.lower⟩
Lower Closure Order Criterion: $\text{lowerClosure}(s) \leq t \leftrightarrow s \subseteq t$
Informal description
For any subset $s$ of a preordered set $\alpha$ and any lower set $t$ of $\alpha$, the lower closure of $s$ is less than or equal to $t$ if and only if $s$ is a subset of $t$. Here, the order on lower sets is given by reverse inclusion, meaning $L \leq M$ if and only if $M \subseteq L$ as sets.
le_upperClosure theorem
{s : UpperSet α} : s ≤ upperClosure t ↔ t ⊆ s
Full source 
@[simp] lemma le_upperClosure {s : UpperSet α} : s ≤ upperClosure t ↔ t ⊆ s :=
  ⟨fun h ↦ subset_upperClosure.trans <| UpperSet.coe_subset_coe.2 h,
    fun h ↦ upperClosure_min h s.upper⟩
Upper Set Ordering via Upper Closure and Subset Relation
Informal description
For any upper set $s$ in a preordered type $\alpha$ and any subset $t$ of $\alpha$, the upper set $s$ is less than or equal to the upper closure of $t$ if and only if $t$ is a subset of $s$. In other words, $s \leq \text{upperClosure}(t) \leftrightarrow t \subseteq s$.
gc_upperClosure_coe theorem
: GaloisConnection (toDual ∘ upperClosure : Set α → (UpperSet α)ᵒᵈ) ((↑) ∘ ofDual)
Full source 
theorem gc_upperClosure_coe :
    GaloisConnection (toDualtoDual ∘ upperClosure : Set α → (UpperSet α)ᵒᵈ) ((↑) ∘ ofDual) :=
  fun _s _t ↦ le_upperClosure
Galois Connection Between Upper Closure and Underlying Set
Informal description
The pair of functions $(f, g)$, where $f$ maps a subset $s$ of a preordered set $\alpha$ to the dual of its upper closure (i.e., $f(s) = \text{upperClosure}(s)^\text{op}$), and $g$ maps an upper set $t$ in the dual order to its underlying set (i.e., $g(t^\text{op}) = t$), forms a Galois connection. This means that for any subset $s$ of $\alpha$ and any upper set $t$ in the dual order, $f(s) \leq t^\text{op}$ if and only if $s \subseteq g(t^\text{op})$.
gc_lowerClosure_coe theorem
: GaloisConnection (lowerClosure : Set α → LowerSet α) (↑)
Full source 
theorem gc_lowerClosure_coe :
    GaloisConnection (lowerClosure : Set α → LowerSet α) (↑) := fun _s _t ↦ lowerClosure_le
Galois Connection Between Lower Closure and Set Coercion
Informal description
The pair of functions `lowerClosure` and the coercion function from lower sets to sets forms a Galois connection. That is, for any subset $s$ of a preordered set $\alpha$ and any lower set $L$ of $\alpha$, we have $\text{lowerClosure}(s) \leq L$ if and only if $s \subseteq L$ (where the order on lower sets is given by reverse inclusion).
giUpperClosureCoe definition
: GaloisInsertion (toDual ∘ upperClosure : Set α → (UpperSet α)ᵒᵈ) ((↑) ∘ ofDual)
Full source 
/-- `upperClosure` forms a reversed Galois insertion with the coercion from upper sets to sets. -/
def giUpperClosureCoe :
    GaloisInsertion (toDualtoDual ∘ upperClosure : Set α → (UpperSet α)ᵒᵈ) ((↑) ∘ ofDual) where
  choice s hs := toDual (⟨s, fun a _b hab ha => hs ⟨a, ha, hab⟩⟩ : UpperSet α)
  gc := gc_upperClosure_coe
  le_l_u _ := subset_upperClosure
  choice_eq _s hs := ofDual.injective <| SetLike.coe_injective <| subset_upperClosure.antisymm hs
Galois insertion between upper closure and set coercion
Informal description
The pair of functions $(f, g)$, where $f$ maps a subset $s$ of a preordered set $\alpha$ to the dual of its upper closure (i.e., $f(s) = \text{upperClosure}(s)^\text{op}$), and $g$ maps an upper set $t$ in the dual order to its underlying set (i.e., $g(t^\text{op}) = t$), forms a Galois insertion. This means that: 1. $f$ and $g$ form a Galois connection (as in `gc_upperClosure_coe`), 2. For any subset $s$, the underlying set of $f(s)$ contains $s$ (i.e., $s \subseteq g(f(s))$), and 3. The choice function for $f$ is defined canonically as the minimal upper set containing $s$.
giLowerClosureCoe definition
: GaloisInsertion (lowerClosure : Set α → LowerSet α) (↑)
Full source 
/-- `lowerClosure` forms a Galois insertion with the coercion from lower sets to sets. -/
def giLowerClosureCoe : GaloisInsertion (lowerClosure : Set α → LowerSet α) (↑) where
  choice s hs := ⟨s, fun a _b hba ha => hs ⟨a, ha, hba⟩⟩
  gc := gc_lowerClosure_coe
  le_l_u _ := subset_lowerClosure
  choice_eq _s hs := SetLike.coe_injective <| subset_lowerClosure.antisymm hs
Galois Insertion Between Lower Closure and Set Coercion
Informal description
The pair of functions `lowerClosure` and the coercion function from lower sets to sets forms a Galois insertion. That is, for any subset $s$ of a preordered set $\alpha$, the lower closure of $s$ is the smallest lower set containing $s$, and the coercion function is the right adjoint in this Galois connection. Specifically: 1. The function `lowerClosure` is order-preserving (monotone). 2. For any subset $s$, $s$ is contained in its lower closure. 3. The pair satisfies the Galois connection property: for any subset $s$ and lower set $L$, $\text{lowerClosure}(s) \leq L$ if and only if $s \subseteq L$.
upperClosure_anti theorem
: Antitone (upperClosure : Set α → UpperSet α)
Full source 
theorem upperClosure_anti : Antitone (upperClosure : Set α → UpperSet α) :=
  gc_upperClosure_coe.monotone_l
Antitonicity of Upper Closure
Informal description
The function `upperClosure` that maps a subset $s$ of a preordered type $\alpha$ to its upper closure is antitone, meaning that for any subsets $s$ and $t$ of $\alpha$, if $s \subseteq t$ then the upper closure of $t$ is contained in the upper closure of $s$ (as upper sets).
lowerClosure_mono theorem
: Monotone (lowerClosure : Set α → LowerSet α)
Full source 
theorem lowerClosure_mono : Monotone (lowerClosure : Set α → LowerSet α) :=
  gc_lowerClosure_coe.monotone_l
Monotonicity of Lower Closure
Informal description
The function `lowerClosure`, which maps a subset $s$ of a preordered set $\alpha$ to its lower closure, is monotone. That is, for any subsets $s$ and $t$ of $\alpha$, if $s \subseteq t$, then the lower closure of $s$ is contained in the lower closure of $t$ (where containment is with respect to the order on lower sets given by reverse inclusion of the underlying sets).
upperClosure_empty theorem
: upperClosure (∅ : Set α) = ⊤
Full source 
@[simp]
theorem upperClosure_empty : upperClosure (∅ : Set α) = ⊤ :=
  (@gc_upperClosure_coe α).l_bot
Upper Closure of Empty Set is Top Element
Informal description
The upper closure of the empty set in a preordered type $\alpha$ is equal to the greatest upper set (the top element in the lattice of upper sets).
lowerClosure_empty theorem
: lowerClosure (∅ : Set α) = ⊥
Full source 
@[simp]
theorem lowerClosure_empty : lowerClosure (∅ : Set α) = ⊥ :=
  (@gc_lowerClosure_coe α).l_bot
Lower Closure of Empty Set is Bottom Element
Informal description
The lower closure of the empty set in a preordered set $\alpha$ is equal to the bottom element of the lattice of lower sets of $\alpha$.
upperClosure_singleton theorem
(a : α) : upperClosure ({ a } : Set α) = UpperSet.Ici a
Full source 
@[simp]
theorem upperClosure_singleton (a : α) : upperClosure ({a} : Set α) = UpperSet.Ici a := by
  ext
  simp
Upper Closure of Singleton Equals Principal Upper Set
Informal description
For any element $a$ in a preorder $\alpha$, the upper closure of the singleton set $\{a\}$ is equal to the principal upper set $[a, \infty)$, i.e., the set of all elements $x$ in $\alpha$ such that $a \leq x$.
lowerClosure_singleton theorem
(a : α) : lowerClosure ({ a } : Set α) = LowerSet.Iic a
Full source 
@[simp]
theorem lowerClosure_singleton (a : α) : lowerClosure ({a} : Set α) = LowerSet.Iic a := by
  ext
  simp
Lower Closure of Singleton Equals Principal Lower Set
Informal description
For any element $a$ in a preorder $\alpha$, the lower closure of the singleton set $\{a\}$ is equal to the principal lower set $(-\infty, a]$, i.e., the set of all elements $x$ in $\alpha$ such that $x \leq a$.
upperClosure_univ theorem
: upperClosure (univ : Set α) = ⊥
Full source 
@[simp]
theorem upperClosure_univ : upperClosure (univ : Set α) = ⊥ :=
  bot_unique subset_upperClosure
Upper Closure of Universal Set is Bottom Element
Informal description
For any preordered type $\alpha$, the upper closure of the universal set $\text{univ} : \text{Set} \alpha$ is equal to the bottom element $\bot$ of the lattice of upper sets.
lowerClosure_univ theorem
: lowerClosure (univ : Set α) = ⊤
Full source 
@[simp]
theorem lowerClosure_univ : lowerClosure (univ : Set α) = ⊤ :=
  top_unique subset_lowerClosure
Lower Closure of Universal Set is the Greatest Lower Set
Informal description
For any preordered type $\alpha$, the lower closure of the universal set $\text{univ} : \text{Set} \alpha$ is equal to the greatest lower set $\top$. In other words, $\text{lowerClosure}(\text{univ}) = \top$.
upperClosure_eq_top_iff theorem
: upperClosure s = ⊤ ↔ s = ∅
Full source 
@[simp]
theorem upperClosure_eq_top_iff : upperClosureupperClosure s = ⊤ ↔ s = ∅ :=
  (@gc_upperClosure_coe α _).l_eq_bot.trans subset_empty_iff
Characterization of Greatest Upper Closure: $\text{upperClosure}(s) = \top \leftrightarrow s = \emptyset$
Informal description
For any subset $s$ of a preordered set $\alpha$, the upper closure of $s$ is equal to the greatest upper set $\top$ if and only if $s$ is the empty set. In other words, $\text{upperClosure}(s) = \top \leftrightarrow s = \emptyset$.
lowerClosure_eq_bot_iff theorem
: lowerClosure s = ⊥ ↔ s = ∅
Full source 
@[simp]
theorem lowerClosure_eq_bot_iff : lowerClosurelowerClosure s = ⊥ ↔ s = ∅ :=
  (@gc_lowerClosure_coe α _).l_eq_bot.trans subset_empty_iff
Characterization of Empty Set via Lower Closure: $\text{lowerClosure}(s) = \bot \leftrightarrow s = \emptyset$
Informal description
For any subset $s$ of a preordered set $\alpha$, the lower closure of $s$ is equal to the least lower set $\bot$ if and only if $s$ is the empty set. That is, $\text{lowerClosure}(s) = \bot \leftrightarrow s = \emptyset$.
upperClosure_union theorem
(s t : Set α) : upperClosure (s ∪ t) = upperClosure s ⊓ upperClosure t
Full source 
@[simp]
theorem upperClosure_union (s t : Set α) : upperClosure (s ∪ t) = upperClosureupperClosure s ⊓ upperClosure t :=
  (@gc_upperClosure_coe α _).l_sup
Upper Closure of Union Equals Infimum of Upper Closures
Informal description
For any two subsets $s$ and $t$ of a preordered set $\alpha$, the upper closure of their union $s \cup t$ is equal to the infimum (with respect to the reverse inclusion order) of the upper closures of $s$ and $t$, i.e., $\text{upperClosure}(s \cup t) = \text{upperClosure}(s) \sqcap \text{upperClosure}(t)$.
lowerClosure_union theorem
(s t : Set α) : lowerClosure (s ∪ t) = lowerClosure s ⊔ lowerClosure t
Full source 
@[simp]
theorem lowerClosure_union (s t : Set α) : lowerClosure (s ∪ t) = lowerClosurelowerClosure s ⊔ lowerClosure t :=
  (@gc_lowerClosure_coe α _).l_sup
Lower Closure of Union Equals Supremum of Lower Closures
Informal description
For any two subsets $s$ and $t$ of a partially ordered set $\alpha$, the lower closure of their union $s \cup t$ is equal to the supremum of the lower closures of $s$ and $t$ in the complete lattice of lower sets of $\alpha$.
upperClosure_iUnion theorem
(f : ι → Set α) : upperClosure (⋃ i, f i) = ⨅ i, upperClosure (f i)
Full source 
@[simp]
theorem upperClosure_iUnion (f : ι → Set α) : upperClosure (⋃ i, f i) = ⨅ i, upperClosure (f i) :=
  (@gc_upperClosure_coe α _).l_iSup
Upper Closure of Union Equals Infimum of Upper Closures
Informal description
For any family of sets $(f_i)_{i \in \iota}$ in a preordered type $\alpha$, the upper closure of their union $\bigcup_{i \in \iota} f_i$ is equal to the infimum (with respect to reverse inclusion) of the upper closures of the individual sets $f_i$. That is, $$\text{upperClosure}\left(\bigcup_{i \in \iota} f_i\right) = \bigsqcap_{i \in \iota} \text{upperClosure}(f_i).$$
lowerClosure_iUnion theorem
(f : ι → Set α) : lowerClosure (⋃ i, f i) = ⨆ i, lowerClosure (f i)
Full source 
@[simp]
theorem lowerClosure_iUnion (f : ι → Set α) : lowerClosure (⋃ i, f i) = ⨆ i, lowerClosure (f i) :=
  (@gc_lowerClosure_coe α _).l_iSup
Lower Closure Preserves Union
Informal description
For any family of sets $\{f_i\}_{i \in \iota}$ in a preordered set $\alpha$, the lower closure of their union is equal to the supremum of the lower closures of each individual set $f_i$. That is, \[ \text{lowerClosure}\left(\bigcup_{i} f_i\right) = \bigsqcup_{i} \text{lowerClosure}(f_i). \]
upperClosure_sUnion theorem
(S : Set (Set α)) : upperClosure (⋃₀ S) = ⨅ s ∈ S, upperClosure s
Full source 
@[simp]
theorem upperClosure_sUnion (S : Set (Set α)) : upperClosure (⋃₀ S) = ⨅ s ∈ S, upperClosure s := by
  simp_rw [sUnion_eq_biUnion, upperClosure_iUnion]
Upper Closure of Union Equals Infimum of Upper Closures
Informal description
For any collection of sets $S$ in a preordered type $\alpha$, the upper closure of the union $\bigcup S$ is equal to the infimum (with respect to reverse inclusion) of the upper closures of the individual sets $s \in S$. That is, $$\text{upperClosure}\left(\bigcup S\right) = \bigsqcap_{s \in S} \text{upperClosure}(s).$$
lowerClosure_sUnion theorem
(S : Set (Set α)) : lowerClosure (⋃₀ S) = ⨆ s ∈ S, lowerClosure s
Full source 
@[simp]
theorem lowerClosure_sUnion (S : Set (Set α)) : lowerClosure (⋃₀ S) = ⨆ s ∈ S, lowerClosure s := by
  simp_rw [sUnion_eq_biUnion, lowerClosure_iUnion]
Lower Closure Preserves Union over a Set of Sets
Informal description
For any collection of sets $S$ in a preordered set $\alpha$, the lower closure of the union of all sets in $S$ is equal to the supremum of the lower closures of each individual set in $S$. That is, \[ \text{lowerClosure}\left(\bigcup_{s \in S} s\right) = \bigsqcup_{s \in S} \text{lowerClosure}(s). \]
Set.OrdConnected.upperClosure_inter_lowerClosure theorem
(h : s.OrdConnected) : ↑(upperClosure s) ∩ ↑(lowerClosure s) = s
Full source 
theorem Set.OrdConnected.upperClosure_inter_lowerClosure (h : s.OrdConnected) :
    ↑(upperClosure s) ∩ ↑(lowerClosure s) = s :=
  (subset_inter subset_upperClosure subset_lowerClosure).antisymm'
    fun _a ⟨⟨_b, hb, hba⟩, _c, hc, hac⟩ => h.out hb hc ⟨hba, hac⟩
Intersection of Upper and Lower Closures of an Order-Connected Set
Informal description
For an order-connected subset $s$ of a partially ordered set $\alpha$, the intersection of the upper closure and lower closure of $s$ is equal to $s$ itself, i.e., $\text{upperClosure}(s) \cap \text{lowerClosure}(s) = s$.
ordConnected_iff_upperClosure_inter_lowerClosure theorem
: s.OrdConnected ↔ ↑(upperClosure s) ∩ ↑(lowerClosure s) = s
Full source 
theorem ordConnected_iff_upperClosure_inter_lowerClosure :
    s.OrdConnected ↔ ↑(upperClosure s) ∩ ↑(lowerClosure s) = s := by
  refine ⟨Set.OrdConnected.upperClosure_inter_lowerClosure, fun h => ?_⟩
  rw [← h]
  exact (UpperSet.upper _).ordConnected.inter (LowerSet.lower _).ordConnected
Characterization of Order-Connected Sets via Upper and Lower Closures
Informal description
A subset $s$ of a partially ordered set $\alpha$ is order connected if and only if the intersection of its upper closure and lower closure equals $s$ itself, i.e., $\text{upperClosure}(s) \cap \text{lowerClosure}(s) = s$.
upperBounds_lowerClosure theorem
: upperBounds (lowerClosure s : Set α) = upperBounds s
Full source 
@[simp]
theorem upperBounds_lowerClosure : upperBounds (lowerClosure s : Set α) = upperBounds s :=
  (upperBounds_mono_set subset_lowerClosure).antisymm
    fun _a ha _b ⟨_c, hc, hcb⟩ ↦ hcb.trans <| ha hc
Upper Bounds of Lower Closure Equal Upper Bounds of Original Set
Informal description
For any subset $s$ of a partially ordered set, the set of upper bounds of the lower closure of $s$ is equal to the set of upper bounds of $s$ itself, i.e., $\text{upperBounds}(\text{lowerClosure}(s)) = \text{upperBounds}(s)$.
lowerBounds_upperClosure theorem
: lowerBounds (upperClosure s : Set α) = lowerBounds s
Full source 
@[simp]
theorem lowerBounds_upperClosure : lowerBounds (upperClosure s : Set α) = lowerBounds s :=
  (lowerBounds_mono_set subset_upperClosure).antisymm
    fun _a ha _b ⟨_c, hc, hcb⟩ ↦ (ha hc).trans hcb
Lower Bounds of Upper Closure Equal Lower Bounds of Original Set
Informal description
For any subset $s$ of a partially ordered set $\alpha$, the set of lower bounds of the upper closure of $s$ is equal to the set of lower bounds of $s$ itself, i.e., $\text{lowerBounds}(\text{upperClosure}(s)) = \text{lowerBounds}(s)$.
bddAbove_lowerClosure theorem
: BddAbove (lowerClosure s : Set α) ↔ BddAbove s
Full source 
@[simp]
theorem bddAbove_lowerClosure : BddAboveBddAbove (lowerClosure s : Set α) ↔ BddAbove s := by
  simp_rw [BddAbove, upperBounds_lowerClosure]
Boundedness Above of Lower Closure is Equivalent to Boundedness Above of Original Set
Informal description
For any subset $s$ of a partially ordered set $\alpha$, the lower closure of $s$ is bounded above if and only if $s$ itself is bounded above. In other words, $\text{lowerClosure}(s)$ has an upper bound if and only if $s$ has an upper bound.
bddBelow_upperClosure theorem
: BddBelow (upperClosure s : Set α) ↔ BddBelow s
Full source 
@[simp]
theorem bddBelow_upperClosure : BddBelowBddBelow (upperClosure s : Set α) ↔ BddBelow s := by
  simp_rw [BddBelow, lowerBounds_upperClosure]
Boundedness Below of Upper Closure is Equivalent to Boundedness Below of Original Set
Informal description
For any subset $s$ of a partially ordered set $\alpha$, the upper closure of $s$ is bounded below if and only if $s$ itself is bounded below. In other words, $\text{upperClosure}(s)$ has a lower bound if and only if $s$ has a lower bound.
IsLowerSet.disjoint_upperClosure_left theorem
(ht : IsLowerSet t) : Disjoint (↑(upperClosure s)) t ↔ Disjoint s t
Full source 
@[simp] lemma IsLowerSet.disjoint_upperClosure_left (ht : IsLowerSet t) :
    DisjointDisjoint ↑(upperClosure s) t ↔ Disjoint s t := by
  refine ⟨Disjoint.mono_left subset_upperClosure, ?_⟩
  simp only [disjoint_left, SetLike.mem_coe, mem_upperClosure, forall_exists_index, and_imp]
  exact fun h a b hb hba ha ↦ h hb <| ht hba ha
Disjointness of Upper Closure with Lower Set
Informal description
For any lower set $t$ in a partially ordered set $\alpha$, the upper closure of a set $s$ is disjoint from $t$ if and only if $s$ is disjoint from $t$. In other words, $\text{upperClosure}(s) \cap t = \emptyset \leftrightarrow s \cap t = \emptyset$.
IsLowerSet.disjoint_upperClosure_right theorem
(hs : IsLowerSet s) : Disjoint s (upperClosure t) ↔ Disjoint s t
Full source 
@[simp] lemma IsLowerSet.disjoint_upperClosure_right (hs : IsLowerSet s) :
    DisjointDisjoint s (upperClosure t) ↔ Disjoint s t := by
  simpa only [disjoint_comm] using hs.disjoint_upperClosure_left
Disjointness of Lower Set with Upper Closure
Informal description
For any lower set $s$ in a partially ordered set $\alpha$, the set $s$ is disjoint from the upper closure of a set $t$ if and only if $s$ is disjoint from $t$ itself. In other words, $s \cap \text{upperClosure}(t) = \emptyset \leftrightarrow s \cap t = \emptyset$.
IsUpperSet.disjoint_lowerClosure_left theorem
(ht : IsUpperSet t) : Disjoint (↑(lowerClosure s)) t ↔ Disjoint s t
Full source 
@[simp] lemma IsUpperSet.disjoint_lowerClosure_left (ht : IsUpperSet t) :
    DisjointDisjoint ↑(lowerClosure s) t ↔ Disjoint s t := ht.toDual.disjoint_upperClosure_left
Disjointness of Lower Closure with Upper Set
Informal description
For any upper set $t$ in a partially ordered set $\alpha$, the lower closure of a set $s$ is disjoint from $t$ if and only if $s$ is disjoint from $t$. In other words, $\text{lowerClosure}(s) \cap t = \emptyset \leftrightarrow s \cap t = \emptyset$.
IsUpperSet.disjoint_lowerClosure_right theorem
(hs : IsUpperSet s) : Disjoint s (lowerClosure t) ↔ Disjoint s t
Full source 
@[simp] lemma IsUpperSet.disjoint_lowerClosure_right (hs : IsUpperSet s) :
    DisjointDisjoint s (lowerClosure t) ↔ Disjoint s t := hs.toDual.disjoint_upperClosure_right
Disjointness of Upper Set with Lower Closure
Informal description
For any upper set $s$ in a partially ordered set $\alpha$, the set $s$ is disjoint from the lower closure of a set $t$ if and only if $s$ is disjoint from $t$ itself. In other words, $s \cap \text{lowerClosure}(t) = \emptyset \leftrightarrow s \cap t = \emptyset$.
upperClosure_eq theorem
: ↑(upperClosure s) = s ↔ IsUpperSet s
Full source 
@[simp] lemma upperClosure_eq :
    ↑(upperClosure s) = s ↔ IsUpperSet s :=
  ⟨(· ▸ UpperSet.upper _), IsUpperSet.upperClosure⟩
Characterization of Upper Sets via Upper Closure
Informal description
For a subset $s$ of a partially ordered set $\alpha$, the upper closure of $s$ is equal to $s$ itself if and only if $s$ is an upper set. That is, $\text{upperClosure}(s) = s \leftrightarrow \text{IsUpperSet}(s)$, where $\text{IsUpperSet}(s)$ means that for all $x \in s$ and $y \geq x$, we have $y \in s$.
lowerClosure_eq theorem
: ↑(lowerClosure s) = s ↔ IsLowerSet s
Full source 
@[simp] lemma lowerClosure_eq :
    ↑(lowerClosure s) = s ↔ IsLowerSet s :=
  @upperClosure_eq αᵒᵈ _ _
Characterization of Lower Sets via Lower Closure
Informal description
For a subset $s$ of a partially ordered set $\alpha$, the lower closure of $s$ is equal to $s$ itself if and only if $s$ is a lower set. That is, $\text{lowerClosure}(s) = s \leftrightarrow \text{IsLowerSet}(s)$, where $\text{IsLowerSet}(s)$ means that for all $x \in s$ and $y \leq x$, we have $y \in s$.
IsAntichain.minimal_mem_upperClosure_iff_mem theorem
(hs : IsAntichain (· ≤ ·) s) : Minimal (· ∈ upperClosure s) x ↔ x ∈ s
Full source 
lemma IsAntichain.minimal_mem_upperClosure_iff_mem (hs : IsAntichain (· ≤ ·) s) :
    MinimalMinimal (· ∈ upperClosure s) x ↔ x ∈ s := by
  simp only [upperClosure, UpperSet.mem_mk, mem_setOf_eq]
  refine ⟨fun h ↦ ?_, fun h ↦ ⟨⟨x, h, rfl.le⟩, fun b ⟨a, has, hab⟩ hbx ↦ ?_⟩⟩
  · obtain ⟨a, has, hax⟩ := h.prop
    rwa [h.eq_of_ge ⟨a, has, rfl.le⟩ hax]
  rwa [← hs.eq has h (hab.trans hbx)]
Minimal Elements in Upper Closure of Antichain Coincide with Antichain
Informal description
For an antichain $s$ in a partially ordered set $\alpha$, an element $x$ is minimal in the upper closure of $s$ if and only if $x$ belongs to $s$.
IsAntichain.maximal_mem_lowerClosure_iff_mem theorem
(hs : IsAntichain (· ≤ ·) s) : Maximal (· ∈ lowerClosure s) x ↔ x ∈ s
Full source 
lemma IsAntichain.maximal_mem_lowerClosure_iff_mem (hs : IsAntichain (· ≤ ·) s) :
    MaximalMaximal (· ∈ lowerClosure s) x ↔ x ∈ s :=
  hs.to_dual.minimal_mem_upperClosure_iff_mem
Maximal Elements in Lower Closure of Antichain Coincide with Antichain
Informal description
For an antichain $s$ in a partially ordered set $\alpha$, an element $x$ is maximal in the lower closure of $s$ if and only if $x$ belongs to $s$.
LowerSet.sdiff definition
(s : LowerSet α) (t : Set α) : LowerSet α
Full source 
/-- The biggest lower subset of a lower set `s` disjoint from a set `t`. -/
def sdiff (s : LowerSet α) (t : Set α) : LowerSet α where
  carrier := s \ upperClosure t
  lower' := s.lower.sdiff_of_isUpperSet (upperClosure t).upper
Set difference of a lower set and an upper closure
Informal description
For a lower set \( s \) in a partially ordered type \( \alpha \) and a subset \( t \subseteq \alpha \), the set difference \( s \setminus \text{upperClosure}(t) \) is the largest lower subset of \( s \) that is disjoint from the upper closure of \( t \). Here, \( \text{upperClosure}(t) \) denotes the smallest upper set containing \( t \).
LowerSet.erase definition
(s : LowerSet α) (a : α) : LowerSet α
Full source 
/-- The biggest lower subset of a lower set `s` not containing an element `a`. -/
def erase (s : LowerSet α) (a : α) : LowerSet α where
  carrier := s \ UpperSet.Ici a
  lower' := s.lower.sdiff_of_isUpperSet (UpperSet.Ici a).upper
Lower set with element removed
Informal description
For a lower set \( s \) in a partially ordered type \( \alpha \) and an element \( a \in \alpha \), the operation `LowerSet.erase s a` returns the largest lower subset of \( s \) that does not contain \( a \). Formally, it is defined as the set difference \( s \setminus \text{UpperSet.Ici}(a) \), where \(\text{UpperSet.Ici}(a)\) is the principal upper set generated by \( a \).
LowerSet.coe_sdiff theorem
(s : LowerSet α) (t : Set α) : s.sdiff t = (s : Set α) \ upperClosure t
Full source 
@[simp, norm_cast]
lemma coe_sdiff (s : LowerSet α) (t : Set α) : s.sdiff t = (s : Set α) \ upperClosure t := rfl
Characterization of Lower Set Difference via Upper Closure
Informal description
For a lower set $s$ in a partially ordered type $\alpha$ and a subset $t \subseteq \alpha$, the carrier set of the lower set difference $s \setminus t$ is equal to the set difference of the carrier set of $s$ and the upper closure of $t$, i.e., $(s \setminus t) = s \setminus \text{upperClosure}(t)$.
LowerSet.coe_erase theorem
(s : LowerSet α) (a : α) : s.erase a = (s : Set α) \ UpperSet.Ici a
Full source 
@[simp, norm_cast]
lemma coe_erase (s : LowerSet α) (a : α) : s.erase a = (s : Set α) \ UpperSet.Ici a := rfl
Characterization of Lower Set Erasure via Principal Upper Set
Informal description
For any lower set $s$ in a partially ordered type $\alpha$ and any element $a \in \alpha$, the carrier set of the erased lower set $s \setminus \{a\}$ is equal to the set difference of the carrier set of $s$ and the principal upper set generated by $a$, i.e., $s \setminus \{a\} = s \setminus [a, \infty)$.
LowerSet.sdiff_singleton theorem
(s : LowerSet α) (a : α) : s.sdiff { a } = s.erase a
Full source 
@[simp] lemma sdiff_singleton (s : LowerSet α) (a : α) : s.sdiff {a} = s.erase a := by
  simp [sdiff, erase]
Set Difference of Lower Set and Singleton Upper Closure Equals Erasure
Informal description
For any lower set $s$ in a partially ordered type $\alpha$ and any element $a \in \alpha$, the set difference $s \setminus \text{upperClosure}(\{a\})$ is equal to the largest lower subset of $s$ that does not contain $a$, i.e., $s \setminus [a, \infty) = s \setminus \text{UpperSet.Ici}(a)$.
LowerSet.sdiff_le_left theorem
: s.sdiff t ≤ s
Full source 
lemma sdiff_le_left : s.sdiff t ≤ s := diff_subset
Monotonicity of Lower Set Difference: $s \setminus \text{upperClosure}(t) \subseteq s$
Informal description
For any lower set $s$ in a partially ordered type $\alpha$ and any subset $t \subseteq \alpha$, the set difference $s \setminus \text{upperClosure}(t)$ is contained in $s$.
LowerSet.erase_le theorem
: s.erase a ≤ s
Full source 
lemma erase_le : s.erase a ≤ s := diff_subset
Monotonicity of Lower Set Erasure: $s \setminus [a, \infty) \subseteq s$
Informal description
For any lower set $s$ in a partially ordered type $\alpha$ and any element $a \in \alpha$, the lower set obtained by removing $a$ from $s$ is contained in $s$, i.e., $s \setminus \text{UpperSet.Ici}(a) \subseteq s$.
LowerSet.sdiff_eq_left theorem
: s.sdiff t = s ↔ Disjoint (↑s) t
Full source 
@[simp] protected lemma sdiff_eq_left : s.sdiff t = s ↔ Disjoint ↑s t := by
  simp [← SetLike.coe_set_eq]
Characterization of Set Difference Equality for Lower Sets: $s \setminus \text{upperClosure}(t) = s$ iff $s$ and $t$ are disjoint
Informal description
For a lower set $s$ in a partially ordered type $\alpha$ and a subset $t \subseteq \alpha$, the set difference $s \setminus \text{upperClosure}(t)$ equals $s$ if and only if $s$ is disjoint from $t$.
LowerSet.erase_eq theorem
: s.erase a = s ↔ a ∉ s
Full source 
@[simp] lemma erase_eq : s.erase a = s ↔ a ∉ s := by rw [← sdiff_singleton]; simp [-sdiff_singleton]
Characterization of Lower Set Erasure: $s \setminus [a, \infty) = s$ iff $a \notin s$
Informal description
For a lower set $s$ in a partially ordered type $\alpha$ and an element $a \in \alpha$, the equality $s \setminus \text{UpperSet.Ici}(a) = s$ holds if and only if $a$ does not belong to $s$.
LowerSet.sdiff_lt_left theorem
: s.sdiff t < s ↔ ¬Disjoint (↑s) t
Full source 
@[simp] lemma sdiff_lt_left : s.sdiff t < s ↔ ¬ Disjoint ↑s t :=
  sdiff_le_left.lt_iff_ne.trans LowerSet.sdiff_eq_left.not
Strict Containment of Lower Set Difference: $s \setminus \text{upperClosure}(t) \subsetneq s$ iff $s$ meets $t$
Informal description
For a lower set $s$ in a partially ordered type $\alpha$ and a subset $t \subseteq \alpha$, the set difference $s \setminus \text{upperClosure}(t)$ is strictly contained in $s$ if and only if $s$ is not disjoint from $t$.
LowerSet.erase_lt theorem
: s.erase a < s ↔ a ∈ s
Full source 
@[simp] lemma erase_lt : s.erase a < s ↔ a ∈ s := erase_le.lt_iff_ne.trans erase_eq.not_left
Strict Containment of Lower Set After Removal: $s \setminus [a, \infty) \subsetneq s$ iff $a \in s$
Informal description
For a lower set $s$ in a partially ordered type $\alpha$ and an element $a \in \alpha$, the strict inequality $s \setminus \text{Ici}(a) \subsetneq s$ holds if and only if $a$ belongs to $s$, where $\text{Ici}(a)$ denotes the principal upper set generated by $a$.
LowerSet.sdiff_idem theorem
(s : LowerSet α) (t : Set α) : (s.sdiff t).sdiff t = s.sdiff t
Full source 
@[simp] protected lemma sdiff_idem (s : LowerSet α) (t : Set α) : (s.sdiff t).sdiff t = s.sdiff t :=
  SetLike.coe_injective sdiff_idem
Idempotence of Set Difference for Lower Sets
Informal description
For any lower set $s$ in a partially ordered type $\alpha$ and any subset $t \subseteq \alpha$, the set difference operation is idempotent, i.e., $(s \setminus \text{upperClosure}(t)) \setminus \text{upperClosure}(t) = s \setminus \text{upperClosure}(t)$.
LowerSet.erase_idem theorem
(s : LowerSet α) (a : α) : (s.erase a).erase a = s.erase a
Full source 
@[simp] lemma erase_idem (s : LowerSet α) (a : α) : (s.erase a).erase a = s.erase a :=
  SetLike.coe_injective sdiff_idem
Idempotence of Element Removal in Lower Sets
Informal description
For any lower set $s$ in a partially ordered type $\alpha$ and any element $a \in \alpha$, the operation of removing $a$ from $s$ is idempotent, i.e., $(s \setminus \text{Ici}(a)) \setminus \text{Ici}(a) = s \setminus \text{Ici}(a)$, where $\text{Ici}(a)$ denotes the principal upper set generated by $a$.
LowerSet.sdiff_sup_lowerClosure theorem
(hts : t ⊆ s) (hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t) : s.sdiff t ⊔ lowerClosure t = s
Full source 
lemma sdiff_sup_lowerClosure (hts : t ⊆ s) (hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t) :
    s.sdiff t ⊔ lowerClosure t = s := by
  refine le_antisymm (sup_le sdiff_le_left <| lowerClosure_le.2 hts) fun a ha ↦ ?_
  obtain hat | hat := em (a ∈ t)
  · exact subset_union_right (subset_lowerClosure hat)
  · refine subset_union_left ⟨ha, ?_⟩
    rintro ⟨b, hb, hba⟩
    exact hat <| hst _ ha _ hb hba
Decomposition of Lower Set via Set Difference and Lower Closure: $(s \setminus \text{upperClosure}(t)) \cup \text{lowerClosure}(t) = s$
Informal description
Let $s$ be a lower set in a partially ordered set $\alpha$, and let $t \subseteq s$ be a subset such that for any $b \in s$ and $c \in t$, if $c \leq b$ then $b \in t$. Then the union of the set difference $s \setminus \text{upperClosure}(t)$ and the lower closure of $t$ equals $s$, i.e., $(s \setminus \text{upperClosure}(t)) \cup \text{lowerClosure}(t) = s$.
LowerSet.lowerClosure_sup_sdiff theorem
(hts : t ⊆ s) (hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t) : lowerClosure t ⊔ s.sdiff t = s
Full source 
lemma lowerClosure_sup_sdiff (hts : t ⊆ s) (hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t) :
    lowerClosurelowerClosure t ⊔ s.sdiff t = s := by rw [sup_comm, sdiff_sup_lowerClosure hts hst]
Decomposition of Lower Set via Lower Closure and Set Difference: $\text{lowerClosure}(t) \cup (s \setminus \text{upperClosure}(t)) = s$
Informal description
Let $s$ be a lower set in a partially ordered set $\alpha$, and let $t \subseteq s$ be a subset such that for any $b \in s$ and $c \in t$, if $c \leq b$ then $b \in t$. Then the supremum (union) of the lower closure of $t$ and the set difference $s \setminus \text{upperClosure}(t)$ equals $s$, i.e., $\text{lowerClosure}(t) \cup (s \setminus \text{upperClosure}(t)) = s$.
LowerSet.erase_sup_Iic theorem
(ha : a ∈ s) (has : ∀ b ∈ s, a ≤ b → b = a) : s.erase a ⊔ Iic a = s
Full source 
lemma erase_sup_Iic (ha : a ∈ s) (has : ∀ b ∈ s, a ≤ b → b = a) : s.erase a ⊔ Iic a = s := by
  rw [← lowerClosure_singleton, ← sdiff_singleton, sdiff_sup_lowerClosure] <;> simpa
Decomposition of Lower Set via Erasure and Principal Lower Set: $(s \setminus [a, \infty)) \cup (-\infty, a] = s$
Informal description
Let $s$ be a lower set in a partially ordered set $\alpha$, and let $a \in s$ be an element such that for any $b \in s$, if $a \leq b$ then $b = a$. Then the union of the largest lower subset of $s$ not containing $a$ and the principal lower set $(-\infty, a]$ equals $s$, i.e., $(s \setminus [a, \infty)) \cup (-\infty, a] = s$.
LowerSet.Iic_sup_erase theorem
(ha : a ∈ s) (has : ∀ b ∈ s, a ≤ b → b = a) : Iic a ⊔ s.erase a = s
Full source 
lemma Iic_sup_erase (ha : a ∈ s) (has : ∀ b ∈ s, a ≤ b → b = a) : IicIic a ⊔ s.erase a = s := by
  rw [sup_comm, erase_sup_Iic ha has]
Decomposition of Lower Set via Principal Lower Set and Erasure: $(-\infty, a] \cup (s \setminus [a, \infty)) = s$
Informal description
Let $s$ be a lower set in a partially ordered set $\alpha$, and let $a \in s$ be an element such that for any $b \in s$, if $a \leq b$ then $b = a$. Then the union of the principal lower set $(-\infty, a]$ and the largest lower subset of $s$ not containing $a$ equals $s$, i.e., $(-\infty, a] \cup (s \setminus [a, \infty)) = s$.
UpperSet.sdiff definition
(s : UpperSet α) (t : Set α) : UpperSet α
Full source 
/-- The biggest upper subset of a upper set `s` disjoint from a set `t`. -/
def sdiff (s : UpperSet α) (t : Set α) : UpperSet α where
  carrier := s \ lowerClosure t
  upper' := s.upper.sdiff_of_isLowerSet (lowerClosure t).lower
Upper set difference with lower closure
Informal description
Given an upper set \( s \) in a partially ordered set \( \alpha \) and a subset \( t \subseteq \alpha \), the set difference \( s \setminus \text{lowerClosure}(t) \) is an upper set. Here, \( \text{lowerClosure}(t) \) denotes the smallest lower set containing \( t \), consisting of all elements \( x \in \alpha \) such that there exists \( a \in t \) with \( x \leq a \).
UpperSet.erase definition
(s : UpperSet α) (a : α) : UpperSet α
Full source 
/-- The biggest upper subset of a upper set `s` not containing an element `a`. -/
def erase (s : UpperSet α) (a : α) : UpperSet α where
  carrier := s \ LowerSet.Iic a
  upper' := s.upper.sdiff_of_isLowerSet (LowerSet.Iic a).lower
Upper set erasure of an element
Informal description
For an upper set \( s \) in a preorder \( \alpha \) and an element \( a \in \alpha \), the operation `UpperSet.erase s a` returns the largest upper subset of \( s \) that does not contain \( a \). Concretely, it is defined as the set difference \( s \setminus (-\infty, a] \), where \( (-\infty, a] \) is the principal lower set consisting of all elements \( x \leq a \).
UpperSet.coe_sdiff theorem
(s : UpperSet α) (t : Set α) : s.sdiff t = (s : Set α) \ lowerClosure t
Full source 
@[simp, norm_cast]
lemma coe_sdiff (s : UpperSet α) (t : Set α) : s.sdiff t = (s : Set α) \ lowerClosure t := rfl
Characterization of Upper Set Difference via Lower Closure
Informal description
For any upper set $s$ in a preorder $\alpha$ and any subset $t \subseteq \alpha$, the underlying set of the upper set difference $s \setminus \text{lowerClosure}(t)$ is equal to the set difference $(s : \text{Set } \alpha) \setminus \text{lowerClosure}(t)$.
UpperSet.coe_erase theorem
(s : UpperSet α) (a : α) : s.erase a = (s : Set α) \ LowerSet.Iic a
Full source 
@[simp, norm_cast]
lemma coe_erase (s : UpperSet α) (a : α) : s.erase a = (s : Set α) \ LowerSet.Iic a := rfl
Characterization of Upper Set Erasure via Set Difference: $s \setminus (-\infty, a] = s \setminus \text{Iic}(a)$
Informal description
For an upper set $s$ in a preorder $\alpha$ and an element $a \in \alpha$, the underlying set of the erased upper set $s \setminus (-\infty, a]$ is equal to the set difference $(s : \text{Set } \alpha) \setminus (-\infty, a]$, where $(-\infty, a]$ denotes the principal lower set consisting of all elements $x \leq a$.
UpperSet.sdiff_singleton theorem
(s : UpperSet α) (a : α) : s.sdiff { a } = s.erase a
Full source 
@[simp] lemma sdiff_singleton (s : UpperSet α) (a : α) : s.sdiff {a} = s.erase a := by
  simp [sdiff, erase]
Upper set difference with singleton equals erasure: $s \setminus \text{lowerClosure}(\{a\}) = s \setminus (-\infty, a]$
Informal description
For any upper set $s$ in a preorder $\alpha$ and any element $a \in \alpha$, the set difference $s \setminus \text{lowerClosure}(\{a\})$ is equal to the largest upper subset of $s$ that does not contain $a$, i.e., $s \setminus (-\infty, a]$.
UpperSet.le_sdiff_left theorem
: s ≤ s.sdiff t
Full source 
lemma le_sdiff_left : s ≤ s.sdiff t := diff_subset
Upper Set is Contained in its Difference with Lower Closure
Informal description
For any upper set $s$ in a partially ordered set $\alpha$ and any subset $t \subseteq \alpha$, the upper set $s$ is contained in the set difference $s \setminus \text{lowerClosure}(t)$, where $\text{lowerClosure}(t)$ is the smallest lower set containing $t$.
UpperSet.le_erase theorem
: s ≤ s.erase a
Full source 
lemma le_erase : s ≤ s.erase a := diff_subset
Upper Set is Contained in its Erasure
Informal description
For any upper set $s$ in a preorder $\alpha$ and any element $a \in \alpha$, the upper set $s$ is contained in the largest upper subset of $s$ that does not contain $a$, i.e., $s \subseteq s \setminus (-\infty, a]$.
UpperSet.sdiff_eq_left theorem
: s.sdiff t = s ↔ Disjoint (↑s) t
Full source 
@[simp] protected lemma sdiff_eq_left : s.sdiff t = s ↔ Disjoint ↑s t := by
  simp [← SetLike.coe_set_eq]
Upper Set Difference Equals Original Set if and only if Disjoint with Subset
Informal description
For an upper set $s$ in a partially ordered set $\alpha$ and a subset $t \subseteq \alpha$, the set difference $s \setminus \text{lowerClosure}(t)$ equals $s$ if and only if $s$ and $t$ are disjoint, i.e., $s \cap t = \emptyset$.
UpperSet.erase_eq theorem
: s.erase a = s ↔ a ∉ s
Full source 
@[simp] lemma erase_eq : s.erase a = s ↔ a ∉ s := by rw [← sdiff_singleton]; simp [-sdiff_singleton]
Erasure Equals Original Upper Set if and only if Element Not in Set
Informal description
For an upper set $s$ in a preorder $\alpha$ and an element $a \in \alpha$, the largest upper subset of $s$ not containing $a$ equals $s$ if and only if $a$ is not in $s$. In other words, $s \setminus (-\infty, a] = s$ if and only if $a \notin s$.
UpperSet.lt_sdiff_left theorem
: s < s.sdiff t ↔ ¬Disjoint (↑s) t
Full source 
@[simp] lemma lt_sdiff_left : s < s.sdiff t ↔ ¬ Disjoint ↑s t :=
  le_sdiff_left.gt_iff_ne.trans UpperSet.sdiff_eq_left.not
Strict Inclusion in Upper Set Difference Characterizes Non-Disjointness
Informal description
For an upper set $s$ in a partially ordered set $\alpha$ and a subset $t \subseteq \alpha$, the strict inclusion $s \subset s \setminus \text{lowerClosure}(t)$ holds if and only if $s$ and $t$ are not disjoint, i.e., $s \cap t \neq \emptyset$.
UpperSet.lt_erase theorem
: s < s.erase a ↔ a ∈ s
Full source 
@[simp] lemma lt_erase : s < s.erase a ↔ a ∈ s := le_erase.gt_iff_ne.trans erase_eq.not_left
Strict Erasure Inclusion Characterizes Membership in Upper Set
Informal description
For an upper set $s$ in a preorder $\alpha$ and an element $a \in \alpha$, the strict inclusion $s \subset s \setminus (-\infty, a]$ holds if and only if $a$ belongs to $s$.
UpperSet.sdiff_idem theorem
(s : UpperSet α) (t : Set α) : (s.sdiff t).sdiff t = s.sdiff t
Full source 
@[simp] protected lemma sdiff_idem (s : UpperSet α) (t : Set α) : (s.sdiff t).sdiff t = s.sdiff t :=
  SetLike.coe_injective sdiff_idem
Idempotence of Upper Set Difference with Lower Closure
Informal description
For any upper set $s$ in a partially ordered set $\alpha$ and any subset $t \subseteq \alpha$, the set difference operation satisfies $(s \setminus \text{lowerClosure}(t)) \setminus \text{lowerClosure}(t) = s \setminus \text{lowerClosure}(t)$.
UpperSet.erase_idem theorem
(s : UpperSet α) (a : α) : (s.erase a).erase a = s.erase a
Full source 
@[simp] lemma erase_idem (s : UpperSet α) (a : α) : (s.erase a).erase a = s.erase a :=
  SetLike.coe_injective sdiff_idem
Idempotence of Upper Set Erasure
Informal description
For any upper set $s$ in a preorder $\alpha$ and any element $a \in \alpha$, the operation of erasing $a$ from $s$ is idempotent. That is, applying the erase operation twice, $(s \setminus (-\infty, a]) \setminus (-\infty, a]$, yields the same result as applying it once, $s \setminus (-\infty, a]$.
UpperSet.sdiff_inf_upperClosure theorem
(hts : t ⊆ s) (hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t) : s.sdiff t ⊓ upperClosure t = s
Full source 
lemma sdiff_inf_upperClosure (hts : t ⊆ s) (hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t) :
    s.sdiff t ⊓ upperClosure t = s := by
  refine ge_antisymm (le_inf le_sdiff_left <| le_upperClosure.2 hts) fun a ha ↦ ?_
  obtain hat | hat := em (a ∈ t)
  · exact subset_union_right (subset_upperClosure hat)
  · refine subset_union_left ⟨ha, ?_⟩
    rintro ⟨b, hb, hab⟩
    exact hat <| hst _ ha _ hb hab
Decomposition of Upper Set via Difference and Upper Closure
Informal description
Let $s$ be an upper set and $t$ a subset of a partially ordered set $\alpha$ such that $t \subseteq s$ and for all $b \in s$ and $c \in t$, if $b \leq c$ then $b \in t$. Then the infimum of the set difference $s \setminus \text{lowerClosure}(t)$ and the upper closure of $t$ equals $s$, i.e., $(s \setminus \text{lowerClosure}(t)) \sqcap \text{upperClosure}(t) = s$.
UpperSet.upperClosure_inf_sdiff theorem
(hts : t ⊆ s) (hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t) : upperClosure t ⊓ s.sdiff t = s
Full source 
lemma upperClosure_inf_sdiff (hts : t ⊆ s) (hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t) :
    upperClosureupperClosure t ⊓ s.sdiff t = s := by rw [inf_comm, sdiff_inf_upperClosure hts hst]
Decomposition of Upper Set via Upper Closure and Set Difference
Informal description
Let $\alpha$ be a partially ordered set, $s$ an upper set in $\alpha$, and $t$ a subset of $s$ such that for all $b \in s$ and $c \in t$, if $b \leq c$ then $b \in t$. Then the infimum of the upper closure of $t$ and the set difference $s \setminus \text{lowerClosure}(t)$ equals $s$, i.e., $\text{upperClosure}(t) \sqcap (s \setminus \text{lowerClosure}(t)) = s$.
UpperSet.erase_inf_Ici theorem
(ha : a ∈ s) (has : ∀ b ∈ s, b ≤ a → b = a) : s.erase a ⊓ Ici a = s
Full source 
lemma erase_inf_Ici (ha : a ∈ s) (has : ∀ b ∈ s, b ≤ a → b = a) : s.erase a ⊓ Ici a = s := by
  rw [← upperClosure_singleton, ← sdiff_singleton, sdiff_inf_upperClosure] <;> simpa
Decomposition of Upper Set via Erasure and Principal Upper Set: $s \setminus (-\infty, a] \sqcap [a, \infty) = s$
Informal description
Let $s$ be an upper set in a preorder $\alpha$, and let $a \in s$ be an element such that for any $b \in s$, if $b \leq a$ then $b = a$. Then the infimum of the largest upper subset of $s$ not containing $a$ (i.e., $s \setminus (-\infty, a]$) and the principal upper set $[a, \infty)$ equals $s$, i.e., $(s \setminus (-\infty, a]) \sqcap [a, \infty) = s$.
UpperSet.Ici_inf_erase theorem
(ha : a ∈ s) (has : ∀ b ∈ s, b ≤ a → b = a) : Ici a ⊓ s.erase a = s
Full source 
lemma Ici_inf_erase (ha : a ∈ s) (has : ∀ b ∈ s, b ≤ a → b = a) : IciIci a ⊓ s.erase a = s := by
  rw [inf_comm, erase_inf_Ici ha has]
Decomposition of Upper Set via Principal Upper Set and Erasure: $[a, \infty) \sqcap (s \setminus (-\infty, a]) = s$
Informal description
Let $s$ be an upper set in a preorder $\alpha$, and let $a \in s$ be an element such that for any $b \in s$, if $b \leq a$ then $b = a$. Then the infimum of the principal upper set $[a, \infty)$ and the largest upper subset of $s$ not containing $a$ (i.e., $s \setminus (-\infty, a]$) equals $s$, i.e., $[a, \infty) \sqcap (s \setminus (-\infty, a]) = s$.