doc-next-gen

Mathlib.Order.UpperLower.CompleteLattice

Module docstring

{"# The complete lattice structure on UpperSet/LowerSet

This file defines a completely distributive lattice structure on UpperSet and LowerSet, pulled back across the canonical injection (UpperSet.carrier, LowerSet.carrier) into Set α.

Notes

Upper sets are ordered by reverse inclusion. This convention is motivated by the fact that this makes them order-isomorphic to lower sets and antichains, and matches the convention on Filter. ","### Complement "}

UpperSet.instSetLike instance
: SetLike (UpperSet α) α
Full source 
instance : SetLike (UpperSet α) α where
  coe := UpperSet.carrier
  coe_injective' s t h := by cases s; cases t; congr
Upper Sets as Set-Like Structures
Informal description
For any type $\alpha$ with a preorder, the type `UpperSet α` of upper sets in $\alpha$ can be viewed as a set-like structure, where each upper set $s$ corresponds to a subset of $\alpha$ (its carrier set). This means we can treat elements of `UpperSet α` as subsets of $\alpha$ with the additional property of being upward-closed.
UpperSet.Simps.coe definition
(s : UpperSet α) : Set α
Full source 
/-- See Note [custom simps projection]. -/
def Simps.coe (s : UpperSet α) : Set α := s
Underlying subset of an upper set
Informal description
The function maps an upper set \( s \) in a preordered type \( \alpha \) to its underlying subset of \( \alpha \).
UpperSet.ext theorem
{s t : UpperSet α} : (s : Set α) = t → s = t
Full source 
@[ext]
theorem ext {s t : UpperSet α} : (s : Set α) = t → s = t :=
  SetLike.ext'
Extensionality of Upper Sets via Carrier Sets
Informal description
For any two upper sets $s$ and $t$ in a type $\alpha$ with a preorder, if their underlying carrier sets are equal (i.e., $(s : \text{Set } \alpha) = t$), then $s = t$.
UpperSet.carrier_eq_coe theorem
(s : UpperSet α) : s.carrier = s
Full source 
@[simp]
theorem carrier_eq_coe (s : UpperSet α) : s.carrier = s :=
  rfl
Equality of Upper Set Carrier and Coercion
Informal description
For any upper set $s$ in a preorder $\alpha$, the carrier set of $s$ is equal to $s$ itself when viewed as a subset of $\alpha$.
UpperSet.upper theorem
(s : UpperSet α) : IsUpperSet (s : Set α)
Full source 
@[simp] protected lemma upper (s : UpperSet α) : IsUpperSet (s : Set α) := s.upper'
Upper Sets are Upward-Closed
Informal description
For any upper set $s$ in a preordered type $\alpha$, the carrier set of $s$ is upward-closed, meaning that if $x \leq y$ and $x$ is in $s$, then $y$ is also in $s$.
UpperSet.coe_mk theorem
(s : Set α) (hs) : mk s hs = s
Full source 
@[simp, norm_cast] lemma coe_mk (s : Set α) (hs) : mk s hs = s := rfl
Equality of Upper Set Construction with Original Set
Informal description
For any subset $s$ of a type $\alpha$ and a proof $hs$ that $s$ is an upper set, the carrier set of the upper set constructed from $s$ and $hs$ is equal to $s$ itself.
UpperSet.mem_mk theorem
{s : Set α} (hs) {a : α} : a ∈ mk s hs ↔ a ∈ s
Full source 
@[simp] lemma mem_mk {s : Set α} (hs) {a : α} : a ∈ mk s hsa ∈ mk s hs ↔ a ∈ s := Iff.rfl
Membership in Constructed Upper Set
Informal description
For any subset $s$ of $\alpha$ that is an upper set (i.e., satisfies the upward-closed property `hs`), and for any element $a \in \alpha$, we have $a \in \text{mk}(s, \text{hs})$ if and only if $a \in s$.
LowerSet.instSetLike instance
: SetLike (LowerSet α) α
Full source 
instance : SetLike (LowerSet α) α where
  coe := LowerSet.carrier
  coe_injective' s t h := by cases s; cases t; congr
The Set-like Structure on Lower Sets
Informal description
For any type $\alpha$, the type `LowerSet α` of lower sets in $\alpha$ has a canonical `SetLike` structure, meaning that a lower set can be treated as a set of elements of $\alpha$.
LowerSet.Simps.coe definition
(s : LowerSet α) : Set α
Full source 
/-- See Note [custom simps projection]. -/
def Simps.coe (s : LowerSet α) : Set α := s
Underlying set of a lower set
Informal description
The function maps a lower set \( s \) in a type \( \alpha \) to its underlying set of elements in \( \alpha \).
LowerSet.ext theorem
{s t : LowerSet α} : (s : Set α) = t → s = t
Full source 
@[ext]
theorem ext {s t : LowerSet α} : (s : Set α) = t → s = t :=
  SetLike.ext'
Extensionality of Lower Sets via Underlying Sets
Informal description
For any two lower sets $s$ and $t$ in a type $\alpha$, if their underlying sets (as given by the canonical injection into `Set α`) are equal, then $s$ and $t$ are equal as lower sets.
LowerSet.carrier_eq_coe theorem
(s : LowerSet α) : s.carrier = s
Full source 
@[simp]
theorem carrier_eq_coe (s : LowerSet α) : s.carrier = s :=
  rfl
Equality of Lower Set Carrier and Coercion
Informal description
For any lower set $s$ in a type $\alpha$, the underlying carrier set of $s$ is equal to $s$ itself when viewed as a set in $\alpha$. In other words, $s.\text{carrier} = s$.
LowerSet.lower theorem
(s : LowerSet α) : IsLowerSet (s : Set α)
Full source 
@[simp] protected lemma lower (s : LowerSet α) : IsLowerSet (s : Set α) := s.lower'
Lower Sets are Order-Closed Under Smaller Elements
Informal description
For any lower set $s$ in a type $\alpha$, the underlying set of $s$ is order-closed under taking smaller elements (i.e., if $a \in s$ and $b \leq a$, then $b \in s$).
LowerSet.coe_mk theorem
(s : Set α) (hs) : mk s hs = s
Full source 
@[simp, norm_cast] lemma coe_mk (s : Set α) (hs) : mk s hs = s := rfl
Canonical Injection of Lower Set Construction Equals Original Set
Informal description
For any set $s$ in $\alpha$ and a proof $hs$ that $s$ is a lower set, the canonical injection of the lower set constructed from $s$ and $hs$ is equal to $s$ itself, i.e., $\text{mk}\ s\ hs = s$.
LowerSet.mem_mk theorem
{s : Set α} (hs) {a : α} : a ∈ mk s hs ↔ a ∈ s
Full source 
@[simp] lemma mem_mk {s : Set α} (hs) {a : α} : a ∈ mk s hsa ∈ mk s hs ↔ a ∈ s := Iff.rfl
Membership in Constructed Lower Set
Informal description
For any set $s$ in $\alpha$ and a proof $hs$ that $s$ is a lower set, an element $a \in \alpha$ belongs to the lower set constructed from $s$ (denoted as $\text{mk}\ s\ hs$) if and only if $a$ belongs to $s$.
UpperSet.instMin instance
: Min (UpperSet α)
Full source 
instance : Min (UpperSet α) :=
  ⟨fun s t => ⟨s ∪ t, s.upper.union t.upper⟩⟩
Existence of Minimal Upper Set under Reverse Inclusion
Informal description
For any type $\alpha$ with a preorder, the collection of upper sets in $\alpha$ has a minimal element with respect to the reverse inclusion order.
UpperSet.instTop instance
: Top (UpperSet α)
Full source 
instance : Top (UpperSet α) :=
  ⟨⟨∅, isUpperSet_empty⟩⟩
Greatest Upper Set Existence
Informal description
For any type $\alpha$ with a preorder, the collection of upper sets in $\alpha$ has a greatest element with respect to the reverse inclusion order.
UpperSet.instBot instance
: Bot (UpperSet α)
Full source 
instance : Bot (UpperSet α) :=
  ⟨⟨univ, isUpperSet_univ⟩⟩
Bottom Element in Upper Sets under Reverse Inclusion
Informal description
For any type $\alpha$ with a preorder, the collection of upper sets of $\alpha$ has a bottom element with respect to the reverse inclusion order.
UpperSet.instSupSet instance
: SupSet (UpperSet α)
Full source 
instance : SupSet (UpperSet α) :=
  ⟨fun S => ⟨⋂ s ∈ S, ↑s, isUpperSet_iInter₂ fun s _ => s.upper⟩⟩
Supremum Operation on Upper Sets under Reverse Inclusion
Informal description
For any type $\alpha$ with a preorder, the collection of upper sets in $\alpha$ has a supremum operation with respect to the reverse inclusion order. That is, given a family of upper sets $\{s_i\}_{i \in I}$, their supremum $\bigsqcup_{i \in I} s_i$ is the smallest upper set (under reverse inclusion) that contains all $s_i$.
UpperSet.completeLattice instance
: CompleteLattice (UpperSet α)
Full source 
instance completeLattice : CompleteLattice (UpperSet α) :=
  (toDual.injective.comp SetLike.coe_injective).completeLattice _ (fun _ _ => rfl)
    (fun _ _ => rfl) (fun _ => rfl) (fun _ => rfl) rfl rfl
Complete Lattice Structure on Upper Sets under Reverse Inclusion
Informal description
For any type $\alpha$ with a preorder, the collection of upper sets of $\alpha$ forms a complete lattice under the reverse inclusion order. This means that it has all suprema and infima, and satisfies the complete lattice axioms.
UpperSet.completelyDistribLattice instance
: CompletelyDistribLattice (UpperSet α)
Full source 
instance completelyDistribLattice : CompletelyDistribLattice (UpperSet α) :=
  .ofMinimalAxioms <|
    (toDual.injective.comp SetLike.coe_injective).completelyDistribLatticeMinimalAxioms .of _
      (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ => rfl) rfl rfl
Completely Distributive Lattice Structure on Upper Sets under Reverse Inclusion
Informal description
For any type $\alpha$ with a preorder, the collection of upper sets of $\alpha$ forms a completely distributive lattice under the reverse inclusion order. This means that it satisfies the complete distributivity law: arbitrary infima distribute over arbitrary suprema and vice versa.
UpperSet.instInhabited instance
: Inhabited (UpperSet α)
Full source 
instance : Inhabited (UpperSet α) :=
  ⟨⊥⟩
Nonemptiness of Upper Sets
Informal description
For any type $\alpha$ with a preorder, the collection of upper sets of $\alpha$ is nonempty.
UpperSet.coe_subset_coe theorem
: (s : Set α) ⊆ t ↔ t ≤ s
Full source 
@[simp 1100, norm_cast]
theorem coe_subset_coe : (s : Set α) ⊆ t(s : Set α) ⊆ t ↔ t ≤ s :=
  Iff.rfl
Reverse Inclusion Order on Upper Sets via Carrier Sets
Informal description
For any two upper sets $s$ and $t$ in a preordered type $\alpha$, the inclusion of their carrier sets $s \subseteq t$ holds if and only if $t$ is less than or equal to $s$ in the reverse inclusion order on upper sets.
UpperSet.coe_ssubset_coe theorem
: (s : Set α) ⊂ t ↔ t < s
Full source 
@[simp 1100, norm_cast] lemma coe_ssubset_coe : (s : Set α) ⊂ t(s : Set α) ⊂ t ↔ t < s := Iff.rfl
Strict Reverse Inclusion Order on Upper Sets via Carrier Sets
Informal description
For any two upper sets $s$ and $t$ in a preordered type $\alpha$, the strict inclusion of their carrier sets $s \subset t$ holds if and only if $t$ is strictly less than $s$ in the reverse inclusion order on upper sets.
UpperSet.coe_top theorem
: ((⊤ : UpperSet α) : Set α) = ∅
Full source 
@[simp, norm_cast]
theorem coe_top : ((⊤ : UpperSet α) : Set α) = ∅ :=
  rfl
Greatest Upper Set is Empty Set
Informal description
The carrier set of the greatest upper set in $\alpha$ (with respect to the reverse inclusion order) is equal to the empty set, i.e., $(\top : \text{UpperSet} \alpha) = \emptyset$.
UpperSet.coe_bot theorem
: ((⊥ : UpperSet α) : Set α) = univ
Full source 
@[simp, norm_cast]
theorem coe_bot : ((⊥ : UpperSet α) : Set α) = univ :=
  rfl
Bottom Upper Set is the Universal Set
Informal description
For any preordered type $\alpha$, the carrier set of the bottom element in the lattice of upper sets (ordered by reverse inclusion) is equal to the universal set $\alpha$, i.e., $(\bot : \text{UpperSet} \alpha) = \alpha$.
UpperSet.coe_eq_univ theorem
: (s : Set α) = univ ↔ s = ⊥
Full source 
@[simp, norm_cast]
theorem coe_eq_univ : (s : Set α) = univ ↔ s = ⊥ := by simp [SetLike.ext'_iff]
Characterization of Universal Upper Set as Bottom Element
Informal description
For any upper set $s$ in a type $\alpha$ with a preorder, the carrier set of $s$ is equal to the universal set $\alpha$ if and only if $s$ is the bottom element in the lattice of upper sets ordered by reverse inclusion.
UpperSet.coe_eq_empty theorem
: (s : Set α) = ∅ ↔ s = ⊤
Full source 
@[simp, norm_cast]
theorem coe_eq_empty : (s : Set α) = ∅ ↔ s = ⊤ := by simp [SetLike.ext'_iff]
Characterization of Empty Upper Sets as Greatest Elements
Informal description
For an upper set $s$ in a preorder $\alpha$, the carrier set of $s$ is empty if and only if $s$ is the greatest upper set (with respect to reverse inclusion).
UpperSet.coe_nonempty theorem
: (s : Set α).Nonempty ↔ s ≠ ⊤
Full source 
@[simp, norm_cast] lemma coe_nonempty : (s : Set α).Nonempty ↔ s ≠ ⊤ :=
  nonempty_iff_ne_empty.trans coe_eq_empty.not
Nonempty Upper Set Characterization via Greatest Element
Informal description
For an upper set $s$ in a preorder $\alpha$, the carrier set of $s$ is nonempty if and only if $s$ is not the greatest upper set (with respect to reverse inclusion).
UpperSet.coe_sup theorem
(s t : UpperSet α) : (↑(s ⊔ t) : Set α) = (s : Set α) ∩ t
Full source 
@[simp, norm_cast]
theorem coe_sup (s t : UpperSet α) : (↑(s ⊔ t) : Set α) = (s : Set α) ∩ t :=
  rfl
Supremum of Upper Sets as Intersection of Carriers
Informal description
For any two upper sets $s$ and $t$ in a preordered type $\alpha$, the carrier set of their supremum $s \sqcup t$ (with respect to the reverse inclusion order) equals the intersection of their carrier sets. That is, $$ (s \sqcup t) = s \cap t $$ where $\sqcup$ denotes the supremum in the lattice of upper sets ordered by reverse inclusion, and $\cap$ denotes set intersection.
UpperSet.coe_inf theorem
(s t : UpperSet α) : (↑(s ⊓ t) : Set α) = (s : Set α) ∪ t
Full source 
@[simp, norm_cast]
theorem coe_inf (s t : UpperSet α) : (↑(s ⊓ t) : Set α) = (s : Set α) ∪ t :=
  rfl
Infimum of Upper Sets as Union of Carriers
Informal description
For any two upper sets $s$ and $t$ in a preordered type $\alpha$, the carrier set of their infimum $s \sqcap t$ (with respect to the reverse inclusion order) equals the union of their carrier sets. That is, $$ (s \sqcap t) = s \cup t $$ where $\sqcap$ denotes the infimum in the lattice of upper sets ordered by reverse inclusion, and $\cup$ denotes set union.
UpperSet.coe_sSup theorem
(S : Set (UpperSet α)) : (↑(sSup S) : Set α) = ⋂ s ∈ S, ↑s
Full source 
@[simp, norm_cast]
theorem coe_sSup (S : Set (UpperSet α)) : (↑(sSup S) : Set α) = ⋂ s ∈ S, ↑s :=
  rfl
Supremum of Upper Sets as Intersection of Carriers
Informal description
For any collection $S$ of upper sets in a preordered type $\alpha$, the carrier set of the supremum of $S$ (with respect to the reverse inclusion order) equals the intersection of all carrier sets in $S$. That is, $$ \left(\bigsqcup S\right) = \bigcap_{s \in S} s $$ where $\bigsqcup$ denotes the supremum in the lattice of upper sets ordered by reverse inclusion, and $\bigcap$ denotes set intersection.
UpperSet.coe_sInf theorem
(S : Set (UpperSet α)) : (↑(sInf S) : Set α) = ⋃ s ∈ S, ↑s
Full source 
@[simp, norm_cast]
theorem coe_sInf (S : Set (UpperSet α)) : (↑(sInf S) : Set α) = ⋃ s ∈ S, ↑s :=
  rfl
Infimum of Upper Sets as Union of Carriers
Informal description
For any collection $S$ of upper sets in a preordered type $\alpha$, the carrier set of the infimum of $S$ (with respect to the reverse inclusion order) equals the union of all carrier sets in $S$. That is, $$ \left(\bigsqcap S\right) = \bigcup_{s \in S} s $$ where $\bigsqcap$ denotes the infimum in the lattice of upper sets ordered by reverse inclusion, and $\bigcup$ denotes set union.
UpperSet.coe_iSup theorem
(f : ι → UpperSet α) : (↑(⨆ i, f i) : Set α) = ⋂ i, f i
Full source 
@[simp, norm_cast]
theorem coe_iSup (f : ι → UpperSet α) : (↑(⨆ i, f i) : Set α) = ⋂ i, f i := by simp [iSup]
Supremum of Upper Sets as Intersection of Carriers
Informal description
For any family of upper sets $\{f_i\}_{i \in \iota}$ in a preordered type $\alpha$, the carrier set of their supremum (with respect to the reverse inclusion order) equals the intersection of all carrier sets in the family. That is, $$ \left(\bigsqcup_{i} f_i\right) = \bigcap_{i} f_i $$ where $\bigsqcup$ denotes the supremum in the lattice of upper sets ordered by reverse inclusion, and $\bigcap$ denotes set intersection.
UpperSet.coe_iInf theorem
(f : ι → UpperSet α) : (↑(⨅ i, f i) : Set α) = ⋃ i, f i
Full source 
@[simp, norm_cast]
theorem coe_iInf (f : ι → UpperSet α) : (↑(⨅ i, f i) : Set α) = ⋃ i, f i := by simp [iInf]
Infimum of Upper Sets as Union of Carriers
Informal description
For any family of upper sets $\{f_i\}_{i \in \iota}$ in a preordered type $\alpha$, the carrier set of their infimum (with respect to the reverse inclusion order) equals the union of all carrier sets in the family. That is, $$ \left(\bigsqcap_{i} f_i\right) = \bigcup_{i} f_i $$ where $\bigsqcap$ denotes the infimum in the lattice of upper sets ordered by reverse inclusion, and $\bigcup$ denotes set union.
UpperSet.coe_iSup₂ theorem
(f : ∀ i, κ i → UpperSet α) : (↑(⨆ (i) (j), f i j) : Set α) = ⋂ (i) (j), f i j
Full source 
@[norm_cast]
theorem coe_iSup₂ (f : ∀ i, κ i → UpperSet α) :
    (↑(⨆ (i) (j), f i j) : Set α) = ⋂ (i) (j), f i j := by simp
Supremum of Doubly-Indexed Upper Sets as Intersection of Carriers
Informal description
For any doubly-indexed family of upper sets $\{f_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a preordered type $\alpha$, the carrier set of their supremum (with respect to the reverse inclusion order) equals the intersection of all carrier sets in the family. That is, $$ \left(\bigsqcup_{i,j} f_{i,j}\right) = \bigcap_{i,j} f_{i,j} $$ where $\bigsqcup$ denotes the supremum in the lattice of upper sets ordered by reverse inclusion, and $\bigcap$ denotes set intersection.
UpperSet.coe_iInf₂ theorem
(f : ∀ i, κ i → UpperSet α) : (↑(⨅ (i) (j), f i j) : Set α) = ⋃ (i) (j), f i j
Full source 
@[norm_cast]
theorem coe_iInf₂ (f : ∀ i, κ i → UpperSet α) :
    (↑(⨅ (i) (j), f i j) : Set α) = ⋃ (i) (j), f i j := by simp
Infimum of Doubly-Indexed Upper Sets as Union of Carriers
Informal description
For any doubly-indexed family of upper sets $\{f_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a preordered type $\alpha$, the carrier set of their infimum (with respect to the reverse inclusion order) equals the union of all carrier sets in the family. That is, $$ \left(\bigsqcap_{i,j} f_{i,j}\right) = \bigcup_{i,j} f_{i,j} $$ where $\bigsqcap$ denotes the infimum in the lattice of upper sets ordered by reverse inclusion, and $\bigcup$ denotes set union.
UpperSet.not_mem_top theorem
: a ∉ (⊤ : UpperSet α)
Full source 
@[simp]
theorem not_mem_top : a ∉ (⊤ : UpperSet α) :=
  id
Non-membership in the Greatest Upper Set
Informal description
For any element $a$ of type $\alpha$ and the greatest upper set $\top$ in `UpperSet α`, the element $a$ does not belong to $\top$ (viewed as a subset of $\alpha$).
UpperSet.mem_bot theorem
: a ∈ (⊥ : UpperSet α)
Full source 
@[simp]
theorem mem_bot : a ∈ (⊥ : UpperSet α) :=
  trivial
Membership in Bottom Upper Set
Informal description
For any element $a$ in a preordered type $\alpha$, $a$ belongs to the bottom element $\bot$ of the lattice of upper sets (ordered by reverse inclusion).
UpperSet.mem_sup_iff theorem
: a ∈ s ⊔ t ↔ a ∈ s ∧ a ∈ t
Full source 
@[simp]
theorem mem_sup_iff : a ∈ s ⊔ ta ∈ s ⊔ t ↔ a ∈ s ∧ a ∈ t :=
  Iff.rfl
Membership in Supremum of Upper Sets
Informal description
For any element $a$ in a preordered type $\alpha$ and any upper sets $s$ and $t$ in $\alpha$, $a$ belongs to the supremum $s \sqcup t$ if and only if $a$ belongs to both $s$ and $t$.
UpperSet.mem_inf_iff theorem
: a ∈ s ⊓ t ↔ a ∈ s ∨ a ∈ t
Full source 
@[simp]
theorem mem_inf_iff : a ∈ s ⊓ ta ∈ s ⊓ t ↔ a ∈ s ∨ a ∈ t :=
  Iff.rfl
Membership in Infimum of Upper Sets: $a ∈ s ⊓ t ↔ a ∈ s ∨ a ∈ t$
Informal description
For any element $a$ in a preordered type $\alpha$ and any upper sets $s$ and $t$ in $\alpha$, $a$ belongs to the infimum $s \sqcap t$ if and only if $a$ belongs to either $s$ or $t$.
UpperSet.mem_sSup_iff theorem
: a ∈ sSup S ↔ ∀ s ∈ S, a ∈ s
Full source 
@[simp]
theorem mem_sSup_iff : a ∈ sSup Sa ∈ sSup S ↔ ∀ s ∈ S, a ∈ s :=
  mem_iInter₂
Membership in Supremum of Upper Sets: $a \in \bigsqcup S \leftrightarrow \forall s \in S, a \in s$
Informal description
For any element $a$ in a preordered type $\alpha$ and any collection $S$ of upper sets in $\alpha$, $a$ belongs to the supremum $\bigsqcup S$ if and only if $a$ belongs to every upper set $s \in S$.
UpperSet.mem_sInf_iff theorem
: a ∈ sInf S ↔ ∃ s ∈ S, a ∈ s
Full source 
@[simp]
theorem mem_sInf_iff : a ∈ sInf Sa ∈ sInf S ↔ ∃ s ∈ S, a ∈ s :=
  mem_iUnion₂.trans <| by simp only [exists_prop, SetLike.mem_coe]
Membership in Infimum of Upper Sets: $a \in \bigsqcap S \leftrightarrow \exists s \in S, a \in s$
Informal description
For any element $a$ in a preordered type $\alpha$ and any collection $S$ of upper sets in $\alpha$, $a$ belongs to the infimum $\bigsqcap S$ if and only if there exists an upper set $s \in S$ such that $a \in s$.
UpperSet.mem_iSup_iff theorem
{f : ι → UpperSet α} : (a ∈ ⨆ i, f i) ↔ ∀ i, a ∈ f i
Full source 
@[simp]
theorem mem_iSup_iff {f : ι → UpperSet α} : (a ∈ ⨆ i, f i) ↔ ∀ i, a ∈ f i := by
  rw [← SetLike.mem_coe, coe_iSup]
  exact mem_iInter
Characterization of Membership in Supremum of Upper Sets
Informal description
For any family of upper sets $\{f_i\}_{i \in \iota}$ in a preordered type $\alpha$ and any element $a \in \alpha$, $a$ belongs to the supremum $\bigsqcup_{i} f_i$ if and only if $a$ belongs to every upper set $f_i$ in the family. That is, $$ a \in \bigsqcup_{i} f_i \leftrightarrow \forall i, a \in f_i. $$
UpperSet.mem_iInf_iff theorem
{f : ι → UpperSet α} : (a ∈ ⨅ i, f i) ↔ ∃ i, a ∈ f i
Full source 
@[simp]
theorem mem_iInf_iff {f : ι → UpperSet α} : (a ∈ ⨅ i, f i) ↔ ∃ i, a ∈ f i := by
  rw [← SetLike.mem_coe, coe_iInf]
  exact mem_iUnion
Characterization of Membership in Infimum of Upper Sets: $a \in \bigsqcap_i f_i \leftrightarrow \exists i, a \in f_i$
Informal description
For any family of upper sets $\{f_i\}_{i \in \iota}$ in a preordered type $\alpha$ and any element $a \in \alpha$, $a$ belongs to the infimum $\bigsqcap_{i} f_i$ if and only if there exists an index $i$ such that $a \in f_i$. That is, $$ a \in \bigsqcap_{i} f_i \leftrightarrow \exists i, a \in f_i. $$
UpperSet.mem_iSup₂_iff theorem
{f : ∀ i, κ i → UpperSet α} : (a ∈ ⨆ (i) (j), f i j) ↔ ∀ i j, a ∈ f i j
Full source 
theorem mem_iSup₂_iff {f : ∀ i, κ i → UpperSet α} : (a ∈ ⨆ (i) (j), f i j) ↔ ∀ i j, a ∈ f i j := by
  simp
Characterization of Membership in Supremum of Upper Sets
Informal description
For a family of upper sets $\{f_{i,j}\}_{i,j}$ indexed by $i$ and $j$, an element $a$ belongs to the supremum $\bigsqcup_{i,j} f_{i,j}$ if and only if for all indices $i$ and $j$, $a$ belongs to $f_{i,j}$.
UpperSet.mem_iInf₂_iff theorem
{f : ∀ i, κ i → UpperSet α} : (a ∈ ⨅ (i) (j), f i j) ↔ ∃ i j, a ∈ f i j
Full source 
theorem mem_iInf₂_iff {f : ∀ i, κ i → UpperSet α} : (a ∈ ⨅ (i) (j), f i j) ↔ ∃ i j, a ∈ f i j := by
  simp
Characterization of Membership in Infimum of Upper Sets
Informal description
For a family of upper sets $\{f_{i,j}\}_{i,j}$ indexed by $i$ and $j$, an element $a$ belongs to the infimum $\biginf_{i,j} f_{i,j}$ if and only if there exist indices $i$ and $j$ such that $a \in f_{i,j}$.
UpperSet.codisjoint_coe theorem
: Codisjoint (s : Set α) t ↔ Disjoint s t
Full source 
@[simp, norm_cast]
theorem codisjoint_coe : CodisjointCodisjoint (s : Set α) t ↔ Disjoint s t := by
  simp [disjoint_iff, codisjoint_iff, SetLike.ext'_iff]
Codisjointness of Upper Sets is Equivalent to Disjointness of Their Carriers
Informal description
For any two upper sets $s$ and $t$ in a preorder $\alpha$, the sets $s$ and $t$ are codisjoint (i.e., their union is the entire carrier set) if and only if they are disjoint (i.e., their intersection is empty).
LowerSet.instTop instance
: Top (LowerSet α)
Full source 
instance : Top (LowerSet α) :=
  ⟨⟨univ, fun _ _ _ => id⟩⟩
The Greatest Lower Set is the Entire Set
Informal description
The set of all lower sets in a partially ordered set $\alpha$ has a greatest element, namely the entire set $\alpha$ itself.
LowerSet.instBot instance
: Bot (LowerSet α)
Full source 
instance : Bot (LowerSet α) :=
  ⟨⟨∅, fun _ _ _ => id⟩⟩
Bottom Element in the Lattice of Lower Sets
Informal description
For any type $\alpha$ with a preorder, the collection of lower sets of $\alpha$ has a bottom element with respect to the order on lower sets (which is reverse inclusion of the underlying sets).
LowerSet.completeLattice instance
: CompleteLattice (LowerSet α)
Full source 
instance completeLattice : CompleteLattice (LowerSet α) :=
  SetLike.coe_injective.completeLattice _ (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl)
    (fun _ => rfl) rfl rfl
Complete Lattice Structure on Lower Sets
Informal description
For any preordered type $\alpha$, the collection of lower sets of $\alpha$ forms a complete lattice, where the order is given by reverse inclusion of the underlying sets.
LowerSet.completelyDistribLattice instance
: CompletelyDistribLattice (LowerSet α)
Full source 
instance completelyDistribLattice : CompletelyDistribLattice (LowerSet α) :=
  .ofMinimalAxioms <| SetLike.coe_injective.completelyDistribLatticeMinimalAxioms .of _
    (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ => rfl) rfl rfl
Completely Distributive Lattice Structure on Lower Sets
Informal description
For any preordered type $\alpha$, the collection of lower sets of $\alpha$ forms a completely distributive lattice, where the order is given by reverse inclusion of the underlying sets.
LowerSet.instInhabited instance
: Inhabited (LowerSet α)
Full source 
instance : Inhabited (LowerSet α) :=
  ⟨⊥⟩
Nonemptiness of Lower Sets
Informal description
For any type $\alpha$ with a preorder, the collection of lower sets of $\alpha$ is nonempty.
LowerSet.coe_subset_coe theorem
: (s : Set α) ⊆ t ↔ s ≤ t
Full source 
@[norm_cast] lemma coe_subset_coe : (s : Set α) ⊆ t(s : Set α) ⊆ t ↔ s ≤ t := Iff.rfl
Subset Criterion for Lower Set Ordering
Informal description
For any lower sets $s$ and $t$ in a preordered type $\alpha$, the underlying set of $s$ is a subset of the underlying set of $t$ if and only if $s$ is less than or equal to $t$ in the order on lower sets (which is given by reverse inclusion).
LowerSet.coe_ssubset_coe theorem
: (s : Set α) ⊂ t ↔ s < t
Full source 
@[norm_cast] lemma coe_ssubset_coe : (s : Set α) ⊂ t(s : Set α) ⊂ t ↔ s < t := Iff.rfl
Proper Subset Criterion for Strict Ordering of Lower Sets
Informal description
For any lower sets $s$ and $t$ in a preordered type $\alpha$, the underlying set of $s$ is a proper subset of the underlying set of $t$ if and only if $s$ is strictly less than $t$ in the order on lower sets (which is given by reverse inclusion).
LowerSet.coe_top theorem
: ((⊤ : LowerSet α) : Set α) = univ
Full source 
@[simp, norm_cast]
theorem coe_top : ((⊤ : LowerSet α) : Set α) = univ :=
  rfl
Greatest Lower Set is Universal Set
Informal description
For any partially ordered set $\alpha$, the carrier set of the greatest lower set (denoted $\top$) is equal to the universal set $\alpha$, i.e., $(\top : \text{LowerSet} \alpha) = \text{univ}$.
LowerSet.coe_bot theorem
: ((⊥ : LowerSet α) : Set α) = ∅
Full source 
@[simp, norm_cast]
theorem coe_bot : ((⊥ : LowerSet α) : Set α) = ∅ :=
  rfl
Bottom Lower Set is Empty Set
Informal description
The underlying set of the bottom element in the lattice of lower sets of a type $\alpha$ is the empty set, i.e., $(\bot : \text{LowerSet} \alpha) = \emptyset$.
LowerSet.coe_eq_univ theorem
: (s : Set α) = univ ↔ s = ⊤
Full source 
@[simp, norm_cast]
theorem coe_eq_univ : (s : Set α) = univ ↔ s = ⊤ := by simp [SetLike.ext'_iff]
Characterization of Greatest Lower Set via Universal Set
Informal description
For any lower set $s$ in a partially ordered set $\alpha$, the underlying set of $s$ is equal to the universal set $\text{univ}$ if and only if $s$ is the greatest lower set $\top$.
LowerSet.coe_eq_empty theorem
: (s : Set α) = ∅ ↔ s = ⊥
Full source 
@[simp, norm_cast]
theorem coe_eq_empty : (s : Set α) = ∅ ↔ s = ⊥ := by simp [SetLike.ext'_iff]
Characterization of Empty Lower Sets as Bottom Element
Informal description
For any lower set $s$ in a preordered type $\alpha$, the underlying set of $s$ is empty if and only if $s$ is the bottom element of the lattice of lower sets. In other words, $(s : \text{Set } \alpha) = \emptyset \leftrightarrow s = \bot$.
LowerSet.coe_nonempty theorem
: (s : Set α).Nonempty ↔ s ≠ ⊥
Full source 
@[simp, norm_cast] lemma coe_nonempty : (s : Set α).Nonempty ↔ s ≠ ⊥ :=
  nonempty_iff_ne_empty.trans coe_eq_empty.not
Nonemptiness of Lower Set Characterizes Non-Bottom Elements
Informal description
For any lower set $s$ in a preordered type $\alpha$, the underlying set of $s$ is nonempty if and only if $s$ is not the bottom element of the lattice of lower sets. In other words, $(s : \text{Set } \alpha) \neq \emptyset \leftrightarrow s \neq \bot$.
LowerSet.coe_sup theorem
(s t : LowerSet α) : (↑(s ⊔ t) : Set α) = (s : Set α) ∪ t
Full source 
@[simp, norm_cast]
theorem coe_sup (s t : LowerSet α) : (↑(s ⊔ t) : Set α) = (s : Set α) ∪ t :=
  rfl
Supremum of Two Lower Sets Equals Their Union
Informal description
For any two lower sets $s$ and $t$ in a preordered type $\alpha$, the underlying set of their supremum $s \sqcup t$ (with respect to the reverse inclusion order) is equal to the union of their underlying sets, i.e., $(s \sqcup t) = s \cup t$.
LowerSet.coe_inf theorem
(s t : LowerSet α) : (↑(s ⊓ t) : Set α) = (s : Set α) ∩ t
Full source 
@[simp, norm_cast]
theorem coe_inf (s t : LowerSet α) : (↑(s ⊓ t) : Set α) = (s : Set α) ∩ t :=
  rfl
Infimum of Two Lower Sets Equals Their Intersection
Informal description
For any two lower sets $s$ and $t$ in a preordered type $\alpha$, the underlying set of their infimum $s \sqcap t$ (with respect to the reverse inclusion order) is equal to the intersection of their underlying sets, i.e., $(s \sqcap t) = s \cap t$.
LowerSet.coe_sSup theorem
(S : Set (LowerSet α)) : (↑(sSup S) : Set α) = ⋃ s ∈ S, ↑s
Full source 
@[simp, norm_cast]
theorem coe_sSup (S : Set (LowerSet α)) : (↑(sSup S) : Set α) = ⋃ s ∈ S, ↑s :=
  rfl
Supremum of Collection of Lower Sets Equals Union of Their Carrier Sets
Informal description
For any collection $S$ of lower sets in a preordered type $\alpha$, the underlying set of the supremum of $S$ is equal to the union of the underlying sets of all lower sets in $S$. That is, $$ \left(\bigsqcup S\right) = \bigcup_{s \in S} s $$ where $\bigsqcup$ denotes the supremum in the lattice of lower sets (ordered by reverse inclusion) and $\bigcup$ denotes the set-theoretic union.
LowerSet.coe_sInf theorem
(S : Set (LowerSet α)) : (↑(sInf S) : Set α) = ⋂ s ∈ S, ↑s
Full source 
@[simp, norm_cast]
theorem coe_sInf (S : Set (LowerSet α)) : (↑(sInf S) : Set α) = ⋂ s ∈ S, ↑s :=
  rfl
Infimum of Collection of Lower Sets Equals Intersection of Their Carrier Sets
Informal description
For any collection $S$ of lower sets in a preordered type $\alpha$, the underlying set of the infimum of $S$ is equal to the intersection of the underlying sets of all lower sets in $S$. That is, $$ \left(\bigsqcap S\right) = \bigcap_{s \in S} s $$ where $\bigsqcap$ denotes the infimum in the lattice of lower sets (ordered by reverse inclusion) and $\bigcap$ denotes the set-theoretic intersection.
LowerSet.coe_iSup theorem
(f : ι → LowerSet α) : (↑(⨆ i, f i) : Set α) = ⋃ i, f i
Full source 
@[simp, norm_cast]
theorem coe_iSup (f : ι → LowerSet α) : (↑(⨆ i, f i) : Set α) = ⋃ i, f i := by
  simp_rw [iSup, coe_sSup, mem_range, iUnion_exists, iUnion_iUnion_eq']
Supremum of Family of Lower Sets Equals Union of Their Carrier Sets
Informal description
Let $\alpha$ be a type with a preorder, and let $\{f_i\}_{i \in \iota}$ be a family of lower sets in $\alpha$. The underlying set of the supremum of this family of lower sets is equal to the union of the underlying sets of the individual lower sets, i.e., $$ \left(\bigsqcup_{i} f_i\right) = \bigcup_{i} f_i $$ where $\bigsqcup$ denotes the supremum in the lattice of lower sets (ordered by reverse inclusion) and $\bigcup$ denotes the set-theoretic union.
LowerSet.coe_iInf theorem
(f : ι → LowerSet α) : (↑(⨅ i, f i) : Set α) = ⋂ i, f i
Full source 
@[simp, norm_cast]
theorem coe_iInf (f : ι → LowerSet α) : (↑(⨅ i, f i) : Set α) = ⋂ i, f i := by
  simp_rw [iInf, coe_sInf, mem_range, iInter_exists, iInter_iInter_eq']
Infimum of Family of Lower Sets as Intersection of Carrier Sets
Informal description
For any family of lower sets $\{f_i\}_{i \in \iota}$ in a preordered type $\alpha$, the underlying set of the infimum of this family is equal to the intersection of the underlying sets of the individual lower sets, i.e., $$ \left(\bigsqcap_{i} f_i\right) = \bigcap_{i} f_i $$ where $\bigsqcap$ denotes the infimum in the lattice of lower sets (ordered by reverse inclusion) and $\bigcap$ denotes the set-theoretic intersection.
LowerSet.coe_iSup₂ theorem
(f : ∀ i, κ i → LowerSet α) : (↑(⨆ (i) (j), f i j) : Set α) = ⋃ (i) (j), f i j
Full source 
@[norm_cast]
theorem coe_iSup₂ (f : ∀ i, κ i → LowerSet α) :
    (↑(⨆ (i) (j), f i j) : Set α) = ⋃ (i) (j), f i j := by simp
Supremum of Doubly Indexed Family of Lower Sets Equals Union of Their Carrier Sets
Informal description
Let $\alpha$ be a type with a preorder, and let $\{f_{i,j}\}_{i \in \iota, j \in \kappa_i}$ be a doubly indexed family of lower sets in $\alpha$. The underlying set of the supremum of this family of lower sets is equal to the union of the underlying sets of the individual lower sets, i.e., $$ \left(\bigsqcup_{i,j} f_{i,j}\right) = \bigcup_{i,j} f_{i,j} $$ where $\bigsqcup$ denotes the supremum in the lattice of lower sets (ordered by reverse inclusion) and $\bigcup$ denotes the set-theoretic union.
LowerSet.coe_iInf₂ theorem
(f : ∀ i, κ i → LowerSet α) : (↑(⨅ (i) (j), f i j) : Set α) = ⋂ (i) (j), f i j
Full source 
@[norm_cast]
theorem coe_iInf₂ (f : ∀ i, κ i → LowerSet α) :
    (↑(⨅ (i) (j), f i j) : Set α) = ⋂ (i) (j), f i j := by simp
Infimum of Doubly Indexed Family of Lower Sets as Intersection of Carrier Sets
Informal description
For any doubly indexed family of lower sets $\{f_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a preordered type $\alpha$, the underlying set of the infimum of this family is equal to the intersection of the underlying sets of the individual lower sets, i.e., $$ \left(\bigsqcap_{i,j} f_{i,j}\right) = \bigcap_{i,j} f_{i,j} $$ where $\bigsqcap$ denotes the infimum in the lattice of lower sets (ordered by reverse inclusion) and $\bigcap$ denotes the set-theoretic intersection.
LowerSet.mem_top theorem
: a ∈ (⊤ : LowerSet α)
Full source 
@[simp]
theorem mem_top : a ∈ (⊤ : LowerSet α) :=
  trivial
Membership in the Greatest Lower Set
Informal description
For any element $a$ in a partially ordered set $\alpha$, $a$ belongs to the greatest lower set (which is the entire set $\alpha$ itself).
LowerSet.not_mem_bot theorem
: a ∉ (⊥ : LowerSet α)
Full source 
@[simp]
theorem not_mem_bot : a ∉ (⊥ : LowerSet α) :=
  id
Non-membership in Bottom Lower Set
Informal description
For any element $a$ of type $\alpha$, $a$ does not belong to the bottom element $\bot$ of the lattice of lower sets on $\alpha$.
LowerSet.mem_sup_iff theorem
: a ∈ s ⊔ t ↔ a ∈ s ∨ a ∈ t
Full source 
@[simp]
theorem mem_sup_iff : a ∈ s ⊔ ta ∈ s ⊔ t ↔ a ∈ s ∨ a ∈ t :=
  Iff.rfl
Membership in Supremum of Lower Sets: $a \in s \sqcup t \leftrightarrow a \in s \lor a \in t$
Informal description
For any element $a$ in a type $\alpha$ with a preorder, and for any two lower sets $s$ and $t$ of $\alpha$, the element $a$ belongs to the supremum (least upper bound) $s \sqcup t$ if and only if $a$ belongs to $s$ or $a$ belongs to $t$.
LowerSet.mem_inf_iff theorem
: a ∈ s ⊓ t ↔ a ∈ s ∧ a ∈ t
Full source 
@[simp]
theorem mem_inf_iff : a ∈ s ⊓ ta ∈ s ⊓ t ↔ a ∈ s ∧ a ∈ t :=
  Iff.rfl
Characterization of Membership in Infimum of Lower Sets
Informal description
For any element $a$ in a type $\alpha$ with a preorder, and for any two lower sets $s$ and $t$ of $\alpha$, the element $a$ belongs to the infimum (greatest lower bound) $s \sqcap t$ if and only if $a$ belongs to both $s$ and $t$.
LowerSet.mem_sSup_iff theorem
: a ∈ sSup S ↔ ∃ s ∈ S, a ∈ s
Full source 
@[simp]
theorem mem_sSup_iff : a ∈ sSup Sa ∈ sSup S ↔ ∃ s ∈ S, a ∈ s :=
  mem_iUnion₂.trans <| by simp only [exists_prop, SetLike.mem_coe]
Characterization of Membership in Supremum of a Collection of Lower Sets
Informal description
For any element $a$ in a type $\alpha$ with a preorder, and for any collection $S$ of lower sets of $\alpha$, the element $a$ belongs to the supremum (least upper bound) $\bigsqcup S$ if and only if there exists a lower set $s \in S$ such that $a \in s$.
LowerSet.mem_sInf_iff theorem
: a ∈ sInf S ↔ ∀ s ∈ S, a ∈ s
Full source 
@[simp]
theorem mem_sInf_iff : a ∈ sInf Sa ∈ sInf S ↔ ∀ s ∈ S, a ∈ s :=
  mem_iInter₂
Characterization of Membership in Infimum of a Collection of Lower Sets
Informal description
For any element $a$ in a type $\alpha$ with a preorder, and for any collection $S$ of lower sets of $\alpha$, the element $a$ belongs to the infimum (greatest lower bound) $\bigsqcap S$ if and only if $a$ belongs to every lower set $s$ in $S$.
LowerSet.mem_iSup_iff theorem
{f : ι → LowerSet α} : (a ∈ ⨆ i, f i) ↔ ∃ i, a ∈ f i
Full source 
@[simp]
theorem mem_iSup_iff {f : ι → LowerSet α} : (a ∈ ⨆ i, f i) ↔ ∃ i, a ∈ f i := by
  rw [← SetLike.mem_coe, coe_iSup]
  exact mem_iUnion
Characterization of Membership in Supremum of a Family of Lower Sets
Informal description
Let $\alpha$ be a type with a preorder, and let $\{f_i\}_{i \in \iota}$ be a family of lower sets in $\alpha$. For any element $a \in \alpha$, we have $a \in \bigsqcup_i f_i$ if and only if there exists an index $i \in \iota$ such that $a \in f_i$, where $\bigsqcup$ denotes the supremum in the lattice of lower sets (ordered by reverse inclusion).
LowerSet.mem_iInf_iff theorem
{f : ι → LowerSet α} : (a ∈ ⨅ i, f i) ↔ ∀ i, a ∈ f i
Full source 
@[simp]
theorem mem_iInf_iff {f : ι → LowerSet α} : (a ∈ ⨅ i, f i) ↔ ∀ i, a ∈ f i := by
  rw [← SetLike.mem_coe, coe_iInf]
  exact mem_iInter
Characterization of Membership in Infimum of a Family of Lower Sets
Informal description
For any family of lower sets $\{f_i\}_{i \in \iota}$ in a preordered type $\alpha$ and any element $a \in \alpha$, the element $a$ belongs to the infimum $\bigsqcap_i f_i$ if and only if $a$ belongs to $f_i$ for every index $i \in \iota$.
LowerSet.mem_iSup₂_iff theorem
{f : ∀ i, κ i → LowerSet α} : (a ∈ ⨆ (i) (j), f i j) ↔ ∃ i j, a ∈ f i j
Full source 
theorem mem_iSup₂_iff {f : ∀ i, κ i → LowerSet α} : (a ∈ ⨆ (i) (j), f i j) ↔ ∃ i j, a ∈ f i j := by
  simp
Characterization of Membership in Supremum of Lower Sets
Informal description
For a family of lower sets $\{f_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a preorder $\alpha$, an element $a \in \alpha$ belongs to the supremum $\bigsqcup_{i,j} f_{i,j}$ if and only if there exist indices $i$ and $j$ such that $a$ belongs to $f_{i,j}$.
LowerSet.mem_iInf₂_iff theorem
{f : ∀ i, κ i → LowerSet α} : (a ∈ ⨅ (i) (j), f i j) ↔ ∀ i j, a ∈ f i j
Full source 
theorem mem_iInf₂_iff {f : ∀ i, κ i → LowerSet α} : (a ∈ ⨅ (i) (j), f i j) ↔ ∀ i j, a ∈ f i j := by
  simp
Characterization of Membership in Infimum of Lower Sets
Informal description
For a family of lower sets $\{f_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a preorder $\alpha$, an element $a \in \alpha$ belongs to the infimum $\bigsqcap_{i,j} f_{i,j}$ if and only if $a$ belongs to $f_{i,j}$ for every $i$ and $j$.
LowerSet.disjoint_coe theorem
: Disjoint (s : Set α) t ↔ Disjoint s t
Full source 
@[simp, norm_cast]
theorem disjoint_coe : DisjointDisjoint (s : Set α) t ↔ Disjoint s t := by
  simp [disjoint_iff, SetLike.ext'_iff]
Equivalence of Set Disjointness and Lattice Disjointness for Lower Sets
Informal description
For any two lower sets $s$ and $t$ in a preorder $\alpha$, the set-theoretic disjointness of their underlying sets (as elements of `Set α`) is equivalent to their lattice-theoretic disjointness (as elements of `LowerSet α`). In other words, $s \cap t = \emptyset$ if and only if $s$ and $t$ are disjoint in the complete lattice of lower sets.
UpperSet.compl definition
(s : UpperSet α) : LowerSet α
Full source 
/-- The complement of a lower set as an upper set. -/
def UpperSet.compl (s : UpperSet α) : LowerSet α :=
  ⟨sᶜ, s.upper.compl⟩
Complement of an upper set as a lower set
Informal description
For an upper set \( s \) in a preorder \( \alpha \), the complement \( s^{\mathsf{c}} \) is defined as a lower set in \( \alpha \). Here, the carrier set of the complement is the set-theoretic complement of the carrier set of \( s \), and it inherits the property of being downward-closed from the upward-closed property of \( s \).
LowerSet.compl definition
(s : LowerSet α) : UpperSet α
Full source 
/-- The complement of a lower set as an upper set. -/
def LowerSet.compl (s : LowerSet α) : UpperSet α :=
  ⟨sᶜ, s.lower.compl⟩
Complement of a lower set as an upper set
Informal description
For a lower set \( s \) in a type \( \alpha \), the complement \( s^c \) is defined as an upper set, consisting of all elements not in \( s \). This operation preserves the order structure, meaning that the complement of a lower set is indeed an upper set.
UpperSet.coe_compl theorem
(s : UpperSet α) : (s.compl : Set α) = (↑s)ᶜ
Full source 
@[simp]
theorem coe_compl (s : UpperSet α) : (s.compl : Set α) = (↑s)ᶜ :=
  rfl
Complement of Upper Set as Set Complement
Informal description
For any upper set $s$ in a preorder $\alpha$, the underlying set of the complement lower set $s^\mathsf{c}$ is equal to the set-theoretic complement of the underlying set of $s$, i.e., $s^\mathsf{c} = s^c$ (where $s^c$ denotes the complement of $s$ as a subset of $\alpha$).
UpperSet.mem_compl_iff theorem
: a ∈ s.compl ↔ a ∉ s
Full source 
@[simp]
theorem mem_compl_iff : a ∈ s.compla ∈ s.compl ↔ a ∉ s :=
  Iff.rfl
Membership in Complement of Upper Set
Informal description
For any element $a$ in a preorder $\alpha$ and any upper set $s$ in $\alpha$, $a$ belongs to the complement lower set $s^\mathsf{c}$ if and only if $a$ does not belong to $s$.
UpperSet.compl_compl theorem
(s : UpperSet α) : s.compl.compl = s
Full source 
@[simp]
nonrec theorem compl_compl (s : UpperSet α) : s.compl.compl = s :=
  UpperSet.ext <| compl_compl _
Double Complement of Upper Set is Original Set
Informal description
For any upper set $s$ in a preorder $\alpha$, the complement of the complement of $s$ is equal to $s$ itself, i.e., $(s^{\mathsf{c}})^{\mathsf{c}} = s$.
UpperSet.compl_le_compl theorem
: s.compl ≤ t.compl ↔ s ≤ t
Full source 
@[simp]
theorem compl_le_compl : s.compl ≤ t.compl ↔ s ≤ t :=
  compl_subset_compl
Order Reversal via Complement: $s^\mathsf{c} ≤ t^\mathsf{c} ↔ s ≤ t$
Informal description
For any two upper sets $s$ and $t$ in a preorder $\alpha$, the complement lower set of $s$ is less than or equal to the complement lower set of $t$ if and only if $s$ is less than or equal to $t$ in the reverse inclusion order.
UpperSet.compl_sup theorem
(s t : UpperSet α) : (s ⊔ t).compl = s.compl ⊔ t.compl
Full source 
@[simp]
protected theorem compl_sup (s t : UpperSet α) : (s ⊔ t).compl = s.compl ⊔ t.compl :=
  LowerSet.ext compl_inf
Complement Distributes over Supremum of Upper Sets
Informal description
For any two upper sets $s$ and $t$ in a preorder $\alpha$, the complement of their supremum (with respect to the reverse inclusion order) equals the supremum of their complements. That is, $(s \sqcup t)^{\mathsf{c}} = s^{\mathsf{c}} \sqcup t^{\mathsf{c}}$, where the complement operation maps upper sets to lower sets and the supremum on the right is taken in the lattice of lower sets.
UpperSet.compl_inf theorem
(s t : UpperSet α) : (s ⊓ t).compl = s.compl ⊓ t.compl
Full source 
@[simp]
protected theorem compl_inf (s t : UpperSet α) : (s ⊓ t).compl = s.compl ⊓ t.compl :=
  LowerSet.ext compl_sup
Complement Distributes over Infimum of Upper Sets
Informal description
For any two upper sets $s$ and $t$ in a preorder $\alpha$, the complement of their infimum equals the infimum of their complements. That is, $(s \sqcap t)^{\mathsf{c}} = s^{\mathsf{c}} \sqcap t^{\mathsf{c}}$, where the complement operation maps upper sets to lower sets and the infimum on the right is taken in the lattice of lower sets.
UpperSet.compl_top theorem
: (⊤ : UpperSet α).compl = ⊤
Full source 
@[simp]
protected theorem compl_top : (⊤ : UpperSet α).compl = ⊤ :=
  LowerSet.ext compl_empty
Complement of Greatest Upper Set is Greatest Lower Set
Informal description
The complement of the greatest upper set (the entire set $\alpha$) is equal to the greatest lower set (the entire set $\alpha$), i.e., $(\top : \text{UpperSet } \alpha)^{\mathsf{c}} = \top$.
UpperSet.compl_bot theorem
: (⊥ : UpperSet α).compl = ⊥
Full source 
@[simp]
protected theorem compl_bot : (⊥ : UpperSet α).compl = ⊥ :=
  LowerSet.ext compl_univ
Complement of Least Upper Set is Least Lower Set
Informal description
The complement of the least upper set (the empty set) is equal to the least lower set (the empty set), i.e., $(\bot : \text{UpperSet } \alpha)^{\mathsf{c}} = \bot$.
UpperSet.compl_sSup theorem
(S : Set (UpperSet α)) : (sSup S).compl = ⨆ s ∈ S, UpperSet.compl s
Full source 
@[simp]
protected theorem compl_sSup (S : Set (UpperSet α)) : (sSup S).compl = ⨆ s ∈ S, UpperSet.compl s :=
  LowerSet.ext <| by simp only [coe_compl, coe_sSup, compl_iInter₂, LowerSet.coe_iSup₂]
Complement of Supremum of Upper Sets Equals Supremum of Complements
Informal description
For any collection $S$ of upper sets in a preordered type $\alpha$, the complement of the supremum of $S$ (with respect to the reverse inclusion order) is equal to the supremum of the complements of the upper sets in $S$. That is, $$ \left(\bigsqcup_{s \in S} s\right)^{\mathsf{c}} = \bigsqcup_{s \in S} s^{\mathsf{c}} $$ where $\bigsqcup$ denotes the supremum in the lattice of upper sets and $^{\mathsf{c}}$ denotes the complement operation mapping upper sets to lower sets.
UpperSet.compl_sInf theorem
(S : Set (UpperSet α)) : (sInf S).compl = ⨅ s ∈ S, UpperSet.compl s
Full source 
@[simp]
protected theorem compl_sInf (S : Set (UpperSet α)) : (sInf S).compl = ⨅ s ∈ S, UpperSet.compl s :=
  LowerSet.ext <| by simp only [coe_compl, coe_sInf, compl_iUnion₂, LowerSet.coe_iInf₂]
Complement of Infimum of Upper Sets Equals Infimum of Complements
Informal description
For any collection $S$ of upper sets in a preordered type $\alpha$, the complement of the infimum of $S$ (with respect to the reverse inclusion order) is equal to the infimum of the complements of the upper sets in $S$. That is, $$ \left(\bigsqcap_{s \in S} s\right)^{\mathsf{c}} = \bigsqcap_{s \in S} s^{\mathsf{c}} $$ where $\bigsqcap$ denotes the infimum in the lattice of upper sets and $^{\mathsf{c}}$ denotes the complement operation mapping upper sets to lower sets.
UpperSet.compl_iSup theorem
(f : ι → UpperSet α) : (⨆ i, f i).compl = ⨆ i, (f i).compl
Full source 
@[simp]
protected theorem compl_iSup (f : ι → UpperSet α) : (⨆ i, f i).compl = ⨆ i, (f i).compl :=
  LowerSet.ext <| by simp only [coe_compl, coe_iSup, compl_iInter, LowerSet.coe_iSup]
Complement of Supremum of Upper Sets Equals Supremum of Complements
Informal description
Let $\alpha$ be a type with a preorder, and let $\{f_i\}_{i \in \iota}$ be a family of upper sets in $\alpha$. The complement of the supremum of this family of upper sets (with respect to reverse inclusion order) is equal to the supremum of the complements of the individual upper sets. That is, $$ \left(\bigsqcup_{i} f_i\right)^{\mathsf{c}} = \bigsqcup_{i} f_i^{\mathsf{c}} $$ where $\bigsqcup$ denotes the supremum in the lattice of upper sets and $^{\mathsf{c}}$ denotes the complement operation mapping upper sets to lower sets.
UpperSet.compl_iInf theorem
(f : ι → UpperSet α) : (⨅ i, f i).compl = ⨅ i, (f i).compl
Full source 
@[simp]
protected theorem compl_iInf (f : ι → UpperSet α) : (⨅ i, f i).compl = ⨅ i, (f i).compl :=
  LowerSet.ext <| by simp only [coe_compl, coe_iInf, compl_iUnion, LowerSet.coe_iInf]
Complement of Infimum of Upper Sets Equals Infimum of Complements
Informal description
For any family of upper sets $\{f_i\}_{i \in \iota}$ in a preordered type $\alpha$, the complement of the infimum of the family is equal to the infimum of the complements of the individual upper sets. That is, $$ \left(\bigsqcap_{i} f_i\right)^{\mathsf{c}} = \bigsqcap_{i} f_i^{\mathsf{c}} $$ where $\bigsqcap$ denotes the infimum in the lattice of upper sets (ordered by reverse inclusion) and $^{\mathsf{c}}$ denotes the complement operation mapping upper sets to lower sets.
UpperSet.compl_iSup₂ theorem
(f : ∀ i, κ i → UpperSet α) : (⨆ (i) (j), f i j).compl = ⨆ (i) (j), (f i j).compl
Full source 
theorem compl_iSup₂ (f : ∀ i, κ i → UpperSet α) :
    (⨆ (i) (j), f i j).compl = ⨆ (i) (j), (f i j).compl := by simp
Complement of Supremum of Doubly Indexed Upper Sets Equals Supremum of Complements
Informal description
For any doubly indexed family of upper sets $\{f_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a preordered type $\alpha$, the complement of the supremum of the family is equal to the supremum of the complements of the individual upper sets. That is, $$ \left(\bigsqcup_{i,j} f_{i,j}\right)^{\mathsf{c}} = \bigsqcup_{i,j} f_{i,j}^{\mathsf{c}} $$ where $\bigsqcup$ denotes the supremum in the lattice of upper sets (ordered by reverse inclusion) and $^{\mathsf{c}}$ denotes the complement operation mapping upper sets to lower sets.
UpperSet.compl_iInf₂ theorem
(f : ∀ i, κ i → UpperSet α) : (⨅ (i) (j), f i j).compl = ⨅ (i) (j), (f i j).compl
Full source 
theorem compl_iInf₂ (f : ∀ i, κ i → UpperSet α) :
    (⨅ (i) (j), f i j).compl = ⨅ (i) (j), (f i j).compl := by simp
Complement of Infimum of Doubly Indexed Upper Sets Equals Infimum of Complements
Informal description
For any doubly indexed family of upper sets $\{f_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a preordered type $\alpha$, the complement of the infimum of the family is equal to the infimum of the complements of the individual upper sets. That is, $$ \left(\bigsqcap_{i,j} f_{i,j}\right)^{\mathsf{c}} = \bigsqcap_{i,j} f_{i,j}^{\mathsf{c}} $$ where $\bigsqcap$ denotes the infimum in the lattice of upper sets (ordered by reverse inclusion) and $^{\mathsf{c}}$ denotes the complement operation mapping upper sets to lower sets.
LowerSet.coe_compl theorem
(s : LowerSet α) : (s.compl : Set α) = (↑s)ᶜ
Full source 
@[simp]
theorem coe_compl (s : LowerSet α) : (s.compl : Set α) = (↑s)ᶜ :=
  rfl
Complement Correspondence for Lower Sets: $s^\mathrm{compl} = s^c$
Informal description
For any lower set $s$ in a type $\alpha$, the carrier set of its complement (as an upper set) is equal to the set-theoretic complement of the carrier set of $s$, i.e., $(s^\mathrm{compl} : \mathrm{Set} \alpha) = s^c$.
LowerSet.mem_compl_iff theorem
: a ∈ s.compl ↔ a ∉ s
Full source 
@[simp]
theorem mem_compl_iff : a ∈ s.compla ∈ s.compl ↔ a ∉ s :=
  Iff.rfl
Membership in Complement of Lower Set
Informal description
An element $a$ belongs to the complement of a lower set $s$ (viewed as an upper set) if and only if $a$ does not belong to $s$, i.e., $a \in s^\mathrm{compl} \leftrightarrow a \notin s$.
LowerSet.compl_compl theorem
(s : LowerSet α) : s.compl.compl = s
Full source 
@[simp]
nonrec theorem compl_compl (s : LowerSet α) : s.compl.compl = s :=
  LowerSet.ext <| compl_compl _
Double Complement of a Lower Set is Itself
Informal description
For any lower set $s$ in a type $\alpha$, the complement of the complement of $s$ is equal to $s$ itself, i.e., $(s^\mathrm{compl})^\mathrm{compl} = s$.
LowerSet.compl_le_compl theorem
: s.compl ≤ t.compl ↔ s ≤ t
Full source 
@[simp]
theorem compl_le_compl : s.compl ≤ t.compl ↔ s ≤ t :=
  compl_subset_compl
Order Reversal via Complement: $s^c \leq t^c \leftrightarrow s \leq t$
Informal description
For any two lower sets $s$ and $t$ in a preordered type $\alpha$, the complement upper set of $s$ is less than or equal to the complement upper set of $t$ if and only if $s$ is less than or equal to $t$ as lower sets.
LowerSet.compl_sup theorem
(s t : LowerSet α) : (s ⊔ t).compl = s.compl ⊔ t.compl
Full source 
protected theorem compl_sup (s t : LowerSet α) : (s ⊔ t).compl = s.compl ⊔ t.compl :=
  UpperSet.ext compl_sup
Complement Distributes over Supremum of Lower Sets
Informal description
For any two lower sets $s$ and $t$ in a type $\alpha$, the complement of their supremum (union) is equal to the supremum of their complements, i.e., $(s \sqcup t)^c = s^c \sqcup t^c$.
LowerSet.compl_inf theorem
(s t : LowerSet α) : (s ⊓ t).compl = s.compl ⊓ t.compl
Full source 
protected theorem compl_inf (s t : LowerSet α) : (s ⊓ t).compl = s.compl ⊓ t.compl :=
  UpperSet.ext compl_inf
Complement Distributes over Infimum of Lower Sets
Informal description
For any two lower sets $s$ and $t$ in a type $\alpha$ with a preorder, the complement of their infimum (intersection) equals the infimum of their complements, i.e., $(s \sqcap t)^c = s^c \sqcap t^c$.
LowerSet.compl_top theorem
: (⊤ : LowerSet α).compl = ⊤
Full source 
protected theorem compl_top : (⊤ : LowerSet α).compl = ⊤ :=
  UpperSet.ext compl_univ
Complement of the Greatest Lower Set is the Greatest Upper Set
Informal description
The complement of the greatest lower set (the entire set $\alpha$) is the greatest upper set (the entire set $\alpha$), i.e., $(\top : \text{LowerSet } \alpha)^c = \top$.
LowerSet.compl_bot theorem
: (⊥ : LowerSet α).compl = ⊥
Full source 
protected theorem compl_bot : (⊥ : LowerSet α).compl = ⊥ :=
  UpperSet.ext compl_empty
Complement of Bottom Lower Set is Bottom Upper Set
Informal description
The complement of the bottom element in the lattice of lower sets is the bottom element in the lattice of upper sets, i.e., $(\bot : \text{LowerSet } \alpha)^c = \bot$.
LowerSet.compl_sSup theorem
(S : Set (LowerSet α)) : (sSup S).compl = ⨆ s ∈ S, LowerSet.compl s
Full source 
protected theorem compl_sSup (S : Set (LowerSet α)) : (sSup S).compl = ⨆ s ∈ S, LowerSet.compl s :=
  UpperSet.ext <| by simp only [coe_compl, coe_sSup, compl_iUnion₂, UpperSet.coe_iSup₂]
Complement of Supremum of Lower Sets Equals Supremum of Complements
Informal description
For any collection $S$ of lower sets in a preordered type $\alpha$, the complement of the supremum of $S$ is equal to the supremum of the complements of the lower sets in $S$. That is, $$ \left(\bigsqcup S\right)^c = \bigsqcup_{s \in S} s^c $$ where $\bigsqcup$ denotes the supremum in the lattice of lower sets (ordered by reverse inclusion) and $^c$ denotes the complement operation that maps a lower set to an upper set.
LowerSet.compl_sInf theorem
(S : Set (LowerSet α)) : (sInf S).compl = ⨅ s ∈ S, LowerSet.compl s
Full source 
protected theorem compl_sInf (S : Set (LowerSet α)) : (sInf S).compl = ⨅ s ∈ S, LowerSet.compl s :=
  UpperSet.ext <| by simp only [coe_compl, coe_sInf, compl_iInter₂, UpperSet.coe_iInf₂]
Complement of Infimum of Lower Sets Equals Infimum of Complements
Informal description
For any collection $S$ of lower sets in a preordered type $\alpha$, the complement of the infimum of $S$ is equal to the infimum of the complements of the lower sets in $S$. That is, $$ \left(\bigsqcap S\right)^c = \bigsqcap_{s \in S} s^c $$ where $\bigsqcap$ denotes the infimum in the lattice of lower sets (ordered by reverse inclusion) and $^c$ denotes the complement operation that maps a lower set to an upper set.
LowerSet.compl_iSup theorem
(f : ι → LowerSet α) : (⨆ i, f i).compl = ⨆ i, (f i).compl
Full source 
protected theorem compl_iSup (f : ι → LowerSet α) : (⨆ i, f i).compl = ⨆ i, (f i).compl :=
  UpperSet.ext <| by simp only [coe_compl, coe_iSup, compl_iUnion, UpperSet.coe_iSup]
Complement of Supremum of Lower Sets Equals Supremum of Complements
Informal description
Let $\alpha$ be a type with a preorder, and let $\{f_i\}_{i \in \iota}$ be a family of lower sets in $\alpha$. The complement of the supremum of this family of lower sets is equal to the supremum of the complements of the individual lower sets, i.e., $$ \left(\bigsqcup_{i} f_i\right)^c = \bigsqcup_{i} f_i^c $$ where $\bigsqcup$ denotes the supremum in the lattice of lower sets (ordered by reverse inclusion) and $^c$ denotes the complement operation that maps a lower set to an upper set.
LowerSet.compl_iInf theorem
(f : ι → LowerSet α) : (⨅ i, f i).compl = ⨅ i, (f i).compl
Full source 
protected theorem compl_iInf (f : ι → LowerSet α) : (⨅ i, f i).compl = ⨅ i, (f i).compl :=
  UpperSet.ext <| by simp only [coe_compl, coe_iInf, compl_iInter, UpperSet.coe_iInf]
Complement of Infimum of Lower Sets Equals Infimum of Complements
Informal description
For any family of lower sets $\{f_i\}_{i \in \iota}$ in a preordered type $\alpha$, the complement of the infimum of this family is equal to the infimum of the complements of the individual lower sets. That is, $$ \left(\bigsqcap_{i} f_i\right)^c = \bigsqcap_{i} f_i^c $$ where $\bigsqcap$ denotes the infimum in the lattice of lower sets (ordered by reverse inclusion) and $^c$ denotes the complement operation that maps a lower set to an upper set.
LowerSet.compl_iSup₂ theorem
(f : ∀ i, κ i → LowerSet α) : (⨆ (i) (j), f i j).compl = ⨆ (i) (j), (f i j).compl
Full source 
@[simp]
theorem compl_iSup₂ (f : ∀ i, κ i → LowerSet α) :
    (⨆ (i) (j), f i j).compl = ⨆ (i) (j), (f i j).compl := by simp_rw [LowerSet.compl_iSup]
Complement of Supremum of Doubly Indexed Lower Sets Equals Supremum of Complements
Informal description
For any doubly indexed family of lower sets $\{f_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a preordered type $\alpha$, the complement of the supremum of this family is equal to the supremum of the complements of the individual lower sets. That is, $$ \left(\bigsqcup_{i,j} f_{i,j}\right)^c = \bigsqcup_{i,j} f_{i,j}^c $$ where $\bigsqcup$ denotes the supremum in the lattice of lower sets (ordered by reverse inclusion) and $^c$ denotes the complement operation that maps a lower set to an upper set.
LowerSet.compl_iInf₂ theorem
(f : ∀ i, κ i → LowerSet α) : (⨅ (i) (j), f i j).compl = ⨅ (i) (j), (f i j).compl
Full source 
@[simp]
theorem compl_iInf₂ (f : ∀ i, κ i → LowerSet α) :
    (⨅ (i) (j), f i j).compl = ⨅ (i) (j), (f i j).compl := by simp_rw [LowerSet.compl_iInf]
Complement of Infimum of Doubly Indexed Lower Sets Equals Infimum of Complements
Informal description
For any doubly indexed family of lower sets $\{f_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in a preordered type $\alpha$, the complement of the infimum of this family is equal to the infimum of the complements of the individual lower sets. That is, $$ \left(\bigsqcap_{i,j} f_{i,j}\right)^c = \bigsqcap_{i,j} f_{i,j}^c $$ where $\bigsqcap$ denotes the infimum in the lattice of lower sets (ordered by reverse inclusion) and $^c$ denotes the complement operation that maps a lower set to an upper set.
upperSetIsoLowerSet definition
: UpperSet α ≃o LowerSet α
Full source 
/-- Upper sets are order-isomorphic to lower sets under complementation. -/
@[simps]
def upperSetIsoLowerSet : UpperSetUpperSet α ≃o LowerSet α where
  toFun := UpperSet.compl
  invFun := LowerSet.compl
  left_inv := UpperSet.compl_compl
  right_inv := LowerSet.compl_compl
  map_rel_iff' := UpperSet.compl_le_compl
Order isomorphism between upper and lower sets via complementation
Informal description
The order isomorphism between the collection of upper sets and lower sets of a preordered type $\alpha$, where the map sends an upper set to its complement (a lower set) and vice versa. This isomorphism preserves the order structure, meaning that for any two upper sets $s$ and $t$, $s \leq t$ if and only if their complements satisfy the same relation.
UpperSet.isTotal_le instance
: IsTotal (UpperSet α) (· ≤ ·)
Full source 
instance UpperSet.isTotal_le : IsTotal (UpperSet α) (· ≤ ·) := ⟨fun s t => t.upper.total s.upper⟩
Total Order on Upper Sets via Reverse Inclusion
Informal description
For any preordered type $\alpha$, the collection of upper sets of $\alpha$ forms a totally ordered set with respect to the reverse inclusion order.
LowerSet.isTotal_le instance
: IsTotal (LowerSet α) (· ≤ ·)
Full source 
instance LowerSet.isTotal_le : IsTotal (LowerSet α) (· ≤ ·) := ⟨fun s t => s.lower.total t.lower⟩
Total Order on Lower Sets via Inclusion
Informal description
For any preordered type $\alpha$, the collection of lower sets of $\alpha$ forms a totally ordered set with respect to the inclusion order.
UpperSet.instLinearOrder instance
: LinearOrder (UpperSet α)
Full source 
noncomputable instance UpperSet.instLinearOrder : LinearOrder (UpperSet α) := by
  classical exact Lattice.toLinearOrder _
Linear Order Structure on Upper Sets via Reverse Inclusion
Informal description
For any preordered type $\alpha$, the collection of upper sets of $\alpha$ forms a linear order under the reverse inclusion relation.
LowerSet.instLinearOrder instance
: LinearOrder (LowerSet α)
Full source 
noncomputable instance LowerSet.instLinearOrder : LinearOrder (LowerSet α) := by
  classical exact Lattice.toLinearOrder _
Linear Order Structure on Lower Sets via Reverse Inclusion
Informal description
For any preordered type $\alpha$, the collection of lower sets of $\alpha$ forms a linear order with respect to the reverse inclusion order.
UpperSet.instCompleteLinearOrder instance
: CompleteLinearOrder (UpperSet α)
Full source 
noncomputable instance UpperSet.instCompleteLinearOrder : CompleteLinearOrder (UpperSet α) :=
  { completelyDistribLattice, instLinearOrder with }
Complete Linear Order Structure on Upper Sets via Reverse Inclusion
Informal description
For any preordered type $\alpha$, the collection of upper sets of $\alpha$ forms a complete linear order under the reverse inclusion relation. This means that every subset of upper sets has both a supremum and an infimum, and the order is total.
UpperSet.map definition
(f : α ≃o β) : UpperSet α ≃o UpperSet β
Full source 
/-- An order isomorphism of Preorders induces an order isomorphism of their upper sets. -/
def map (f : α ≃o β) : UpperSetUpperSet α ≃o UpperSet β where
  toFun s := ⟨f '' s, s.upper.image f⟩
  invFun t := ⟨f ⁻¹' t, t.upper.preimage f.monotone⟩
  left_inv _ := ext <| f.preimage_image _
  right_inv _ := ext <| f.image_preimage _
  map_rel_iff' := image_subset_image_iff f.injective
Order isomorphism of upper sets induced by an order isomorphism
Informal description
Given an order isomorphism $f : \alpha \simeq \beta$ between preorders $\alpha$ and $\beta$, the function `UpperSet.map` maps an upper set $s$ in $\alpha$ to the upper set $f(s)$ in $\beta$, and its inverse maps an upper set $t$ in $\beta$ to $f^{-1}(t)$ in $\alpha$. This construction yields an order isomorphism between the upper sets of $\alpha$ and the upper sets of $\beta$.
UpperSet.symm_map theorem
(f : α ≃o β) : (map f).symm = map f.symm
Full source 
@[simp]
theorem symm_map (f : α ≃o β) : (map f).symm = map f.symm :=
  DFunLike.ext _ _ fun s => ext <| by convert Set.preimage_equiv_eq_image_symm s f.toEquiv
Inverse of Upper Set Map Equals Map of Inverse
Informal description
For any order isomorphism $f : \alpha \simeq \beta$ between preorders $\alpha$ and $\beta$, the inverse of the induced map on upper sets is equal to the map induced by the inverse isomorphism, i.e., $(\text{map } f)^{-1} = \text{map } f^{-1}$.
UpperSet.mem_map theorem
: b ∈ map f s ↔ f.symm b ∈ s
Full source 
@[simp]
theorem mem_map : b ∈ map f sb ∈ map f s ↔ f.symm b ∈ s := by
  rw [← f.symm_symm, ← symm_map, f.symm_symm]
  rfl
Characterization of Membership in Mapped Upper Set via Order Isomorphism
Informal description
For an order isomorphism $f : \alpha \simeq \beta$ between preorders $\alpha$ and $\beta$, an element $b \in \beta$ belongs to the image of an upper set $s \subseteq \alpha$ under the map $f$ if and only if the inverse image of $b$ under $f$ belongs to $s$. That is, $b \in f(s) \leftrightarrow f^{-1}(b) \in s$.
UpperSet.map_refl theorem
: map (OrderIso.refl α) = OrderIso.refl _
Full source 
@[simp]
theorem map_refl : map (OrderIso.refl α) = OrderIso.refl _ := by
  ext
  simp
Identity Order Isomorphism Maps to Identity on Upper Sets
Informal description
The map operation on upper sets, when applied to the identity order isomorphism $\text{OrderIso.refl } \alpha$, yields the identity order isomorphism on the lattice of upper sets. That is, $\text{map}(\text{OrderIso.refl } \alpha) = \text{OrderIso.refl } (\text{UpperSet } \alpha)$.
UpperSet.map_map theorem
(g : β ≃o γ) (f : α ≃o β) : map g (map f s) = map (f.trans g) s
Full source 
@[simp]
theorem map_map (g : β ≃o γ) (f : α ≃o β) : map g (map f s) = map (f.trans g) s := by
  ext
  simp
Composition of Upper Set Mappings via Order Isomorphisms
Informal description
Given order isomorphisms $f : \alpha \simeq \beta$ and $g : \beta \simeq \gamma$ between preorders $\alpha$, $\beta$, and $\gamma$, the composition of the upper set mappings satisfies $\text{map}_g \circ \text{map}_f = \text{map}_{f \circ g}$.
UpperSet.coe_map theorem
: (map f s : Set β) = f '' s
Full source 
@[simp, norm_cast]
theorem coe_map : (map f s : Set β) = f '' s :=
  rfl
Image of Upper Set Under Order Isomorphism
Informal description
For an order isomorphism $f : \alpha \simeq \beta$ between preorders $\alpha$ and $\beta$, and an upper set $s$ in $\alpha$, the carrier set of the mapped upper set $\text{map}_f(s)$ in $\beta$ equals the image of $s$ under $f$, i.e., $(\text{map}_f(s) : \text{Set } \beta) = f(s)$.
LowerSet.map definition
(f : α ≃o β) : LowerSet α ≃o LowerSet β
Full source 
/-- An order isomorphism of Preorders induces an order isomorphism of their lower sets. -/
def map (f : α ≃o β) : LowerSetLowerSet α ≃o LowerSet β where
  toFun s := ⟨f '' s, s.lower.image f⟩
  invFun t := ⟨f ⁻¹' t, t.lower.preimage f.monotone⟩
  left_inv _ := SetLike.coe_injective <| f.preimage_image _
  right_inv _ := SetLike.coe_injective <| f.image_preimage _
  map_rel_iff' := image_subset_image_iff f.injective
Order isomorphism of lower sets induced by an order isomorphism
Informal description
Given an order isomorphism $f : \alpha \simeq \beta$ between preorders $\alpha$ and $\beta$, the function `LowerSet.map f` is an order isomorphism between the lower sets of $\alpha$ and the lower sets of $\beta$. Specifically: - The forward map sends a lower set $s$ in $\alpha$ to its image $f(s)$ in $\beta$, which remains a lower set. - The inverse map sends a lower set $t$ in $\beta$ to its preimage $f^{-1}(t)$ in $\alpha$, which remains a lower set. - The composition of the forward and inverse maps yields the identity, and the map preserves the order structure.
LowerSet.symm_map theorem
(f : α ≃o β) : (map f).symm = map f.symm
Full source 
@[simp]
theorem symm_map (f : α ≃o β) : (map f).symm = map f.symm :=
  DFunLike.ext _ _ fun s => ext <| by convert Set.preimage_equiv_eq_image_symm s f.toEquiv
Inverse of Lower Set Order Isomorphism Induced by an Order Isomorphism
Informal description
For any order isomorphism $f : \alpha \simeq \beta$ between preorders $\alpha$ and $\beta$, the inverse of the induced order isomorphism on lower sets `LowerSet.map f` is equal to the order isomorphism induced by the inverse of $f$, i.e., $(\text{map } f)^{-1} = \text{map } f^{-1}$.
LowerSet.mem_map theorem
{f : α ≃o β} {b : β} : b ∈ map f s ↔ f.symm b ∈ s
Full source 
@[simp]
theorem mem_map {f : α ≃o β} {b : β} : b ∈ map f sb ∈ map f s ↔ f.symm b ∈ s := by
  rw [← f.symm_symm, ← symm_map, f.symm_symm]
  rfl
Characterization of Membership in Mapped Lower Set via Order Isomorphism
Informal description
For any order isomorphism $f : \alpha \simeq \beta$ between preorders $\alpha$ and $\beta$, and for any element $b \in \beta$, $b$ belongs to the image of a lower set $s$ under the map $f$ if and only if the inverse image of $b$ under $f$ belongs to $s$. In other words, $b \in f(s) \Leftrightarrow f^{-1}(b) \in s$.
LowerSet.map_refl theorem
: map (OrderIso.refl α) = OrderIso.refl _
Full source 
@[simp]
theorem map_refl : map (OrderIso.refl α) = OrderIso.refl _ := by
  ext
  simp
Identity Order Isomorphism Maps to Identity on Lower Sets
Informal description
The map operation on lower sets, when applied to the identity order isomorphism $\text{OrderIso.refl } \alpha$, yields the identity order isomorphism on the lattice of lower sets, i.e., $\text{map}(\text{OrderIso.refl } \alpha) = \text{OrderIso.refl } (\text{LowerSet } \alpha)$.
LowerSet.map_map theorem
(g : β ≃o γ) (f : α ≃o β) : map g (map f s) = map (f.trans g) s
Full source 
@[simp]
theorem map_map (g : β ≃o γ) (f : α ≃o β) : map g (map f s) = map (f.trans g) s := by
  ext
  simp
Composition of Lower Set Maps via Order Isomorphisms
Informal description
For any order isomorphisms $f : \alpha \simeq \beta$ and $g : \beta \simeq \gamma$ between preorders, and for any lower set $s$ in $\alpha$, the image of $s$ under the composition $g \circ f$ is equal to first mapping $s$ under $f$ and then mapping the result under $g$. In other words, $\text{map}_g(\text{map}_f(s)) = \text{map}_{f \circ g}(s)$.
LowerSet.coe_map theorem
: (map f s : Set β) = f '' s
Full source 
@[simp, norm_cast]
theorem coe_map : (map f s : Set β) = f '' s :=
  rfl
Image of Lower Set Under Order Isomorphism Equals Direct Image
Informal description
For an order isomorphism $f : \alpha \simeq \beta$ between preorders $\alpha$ and $\beta$, and a lower set $s$ in $\alpha$, the underlying set of the image of $s$ under the map $f$ is equal to the direct image of $s$ under $f$, i.e., $\text{map}(f)(s) = f(s)$ as subsets of $\beta$.
UpperSet.compl_map theorem
(f : α ≃o β) (s : UpperSet α) : (map f s).compl = LowerSet.map f s.compl
Full source 
@[simp]
theorem compl_map (f : α ≃o β) (s : UpperSet α) : (map f s).compl = LowerSet.map f s.compl :=
  SetLike.coe_injective (Set.image_compl_eq f.bijective).symm
Complement of Image Equals Image of Complement for Upper Sets under Order Isomorphism
Informal description
Let $\alpha$ and $\beta$ be preorders, and let $f : \alpha \simeq \beta$ be an order isomorphism. For any upper set $s$ in $\alpha$, the complement of the image of $s$ under $f$ is equal to the image under $f$ of the complement of $s$. In symbols: $$(f(s))^\mathsf{c} = f(s^\mathsf{c})$$ where $f(s)$ denotes the upper set in $\beta$ obtained by applying $f$ to $s$, and $s^\mathsf{c}$ denotes the complement of $s$ (which is a lower set in $\alpha$).
LowerSet.compl_map theorem
(f : α ≃o β) (s : LowerSet α) : (map f s).compl = UpperSet.map f s.compl
Full source 
@[simp]
theorem compl_map (f : α ≃o β) (s : LowerSet α) : (map f s).compl = UpperSet.map f s.compl :=
  SetLike.coe_injective (Set.image_compl_eq f.bijective).symm
Complement of Image of Lower Set under Order Isomorphism Equals Image of Complement
Informal description
Let $\alpha$ and $\beta$ be preordered types, and let $f : \alpha \simeq \beta$ be an order isomorphism. For any lower set $s$ in $\alpha$, the complement of the image of $s$ under $f$ is equal to the image of the complement of $s$ under $f$ as an upper set. That is, $(f(s))^c = f(s^c)$ as upper sets in $\beta$.