doc-next-gen

Mathlib.Order.Hom.Set

Module docstring

{"# Order homomorphisms and sets "}

Set.sumEquiv definition
: Set (α ⊕ β) ≃o Set α × Set β
Full source 
/-- Sets on sum types are order-equivalent to pairs of sets on each summand. -/
def sumEquiv : SetSet (α ⊕ β) ≃o Set α × Set β where
  toFun s := (Sum.inl ⁻¹' s, Sum.inr ⁻¹' s)
  invFun s := Sum.inlSum.inl '' s.1Sum.inl '' s.1 ∪ Sum.inr '' s.2
  left_inv s := image_preimage_inl_union_image_preimage_inr s
  right_inv s := by
    simp [preimage_image_eq _ Sum.inl_injective, preimage_image_eq _ Sum.inr_injective]
  map_rel_iff' := by simp [subset_def]
Order isomorphism between power set of sum and product of power sets
Informal description
The order isomorphism between the power set of a sum type $\alpha \oplus \beta$ and the product of the power sets of $\alpha$ and $\beta$. Specifically: - The forward map takes a subset $s \subseteq \alpha \oplus \beta$ to the pair $(f^{-1}(s), g^{-1}(s))$ where $f$ and $g$ are the left and right inclusions respectively. - The inverse map takes a pair of subsets $(s_1 \subseteq \alpha, s_2 \subseteq \beta)$ to the union of their images under the left and right inclusions.
OrderIso.range_eq theorem
(e : α ≃o β) : Set.range e = Set.univ
Full source 
theorem range_eq (e : α ≃o β) : Set.range e = Set.univ :=
  e.surjective.range_eq
Range of an Order Isomorphism is the Universal Set
Informal description
For any order isomorphism $e : \alpha \simeq \beta$ between two types $\alpha$ and $\beta$, the range of $e$ is equal to the universal set $\beta$, i.e., $\text{range}(e) = \text{univ}$.
OrderIso.symm_image_image theorem
(e : α ≃o β) (s : Set α) : e.symm '' (e '' s) = s
Full source 
@[simp]
theorem symm_image_image (e : α ≃o β) (s : Set α) : e.symm '' (e '' s) = s :=
  e.toEquiv.symm_image_image s
Preimage of Image under Order Isomorphism is Original Set
Informal description
For any order isomorphism $e : \alpha \simeq \beta$ and any subset $s \subseteq \alpha$, the preimage under $e^{-1}$ of the image of $s$ under $e$ equals $s$, i.e., $e^{-1}(e(s)) = s$.
OrderIso.image_symm_image theorem
(e : α ≃o β) (s : Set β) : e '' (e.symm '' s) = s
Full source 
@[simp]
theorem image_symm_image (e : α ≃o β) (s : Set β) : e '' (e.symm '' s) = s :=
  e.toEquiv.image_symm_image s
Order Isomorphism Image-Preimage Identity: $e(e^{-1}(s)) = s$
Informal description
For any order isomorphism $e : \alpha \simeq \beta$ between ordered types $\alpha$ and $\beta$, and any subset $s \subseteq \beta$, the image under $e$ of the preimage of $s$ under $e^{-1}$ equals $s$ itself. In symbols, $e(e^{-1}(s)) = s$.
OrderIso.image_eq_preimage theorem
(e : α ≃o β) (s : Set α) : e '' s = e.symm ⁻¹' s
Full source 
theorem image_eq_preimage (e : α ≃o β) (s : Set α) : e '' s = e.symm ⁻¹' s :=
  e.toEquiv.image_eq_preimage s
Image Equals Preimage under Order Isomorphism Inverse
Informal description
For any order isomorphism $e \colon \alpha \simeq \beta$ and any subset $s \subseteq \alpha$, the image of $s$ under $e$ is equal to the preimage of $s$ under the inverse order isomorphism $e^{-1}$, i.e., \[ e(s) = e^{-1}^{-1}(s). \]
OrderIso.preimage_symm_preimage theorem
(e : α ≃o β) (s : Set α) : e ⁻¹' (e.symm ⁻¹' s) = s
Full source 
@[simp]
theorem preimage_symm_preimage (e : α ≃o β) (s : Set α) : e ⁻¹' (e.symm ⁻¹' s) = s :=
  e.toEquiv.preimage_symm_preimage s
Double Symmetric Preimage Identity for Order Isomorphisms
Informal description
For any order isomorphism $e : \alpha \simeq \beta$ between ordered sets $\alpha$ and $\beta$, and any subset $s \subseteq \alpha$, the preimage of $s$ under $e^{-1}$ followed by the preimage under $e$ equals $s$. That is, $e^{-1}(e^{-1}(s)) = s$.
OrderIso.symm_preimage_preimage theorem
(e : α ≃o β) (s : Set β) : e.symm ⁻¹' (e ⁻¹' s) = s
Full source 
@[simp]
theorem symm_preimage_preimage (e : α ≃o β) (s : Set β) : e.symm ⁻¹' (e ⁻¹' s) = s :=
  e.toEquiv.symm_preimage_preimage s
Double Preimage Identity for Order Isomorphisms
Informal description
For any order isomorphism $e : \alpha \simeq \beta$ between ordered types $\alpha$ and $\beta$, and any subset $s \subseteq \beta$, the preimage of $s$ under $e$ followed by the preimage under $e^{-1}$ equals $s$. That is, $e^{-1}(e^{-1}(s)) = s$.
OrderIso.image_preimage theorem
(e : α ≃o β) (s : Set β) : e '' (e ⁻¹' s) = s
Full source 
@[simp]
theorem image_preimage (e : α ≃o β) (s : Set β) : e '' (e ⁻¹' s) = s :=
  e.toEquiv.image_preimage s
Order isomorphism preserves image of preimage
Informal description
For any order isomorphism $e : \alpha \simeq \beta$ between partially ordered types $\alpha$ and $\beta$, and any subset $s \subseteq \beta$, the image of the preimage of $s$ under $e$ equals $s$ itself. In symbols, $e(e^{-1}(s)) = s$.
OrderIso.preimage_image theorem
(e : α ≃o β) (s : Set α) : e ⁻¹' (e '' s) = s
Full source 
@[simp]
theorem preimage_image (e : α ≃o β) (s : Set α) : e ⁻¹' (e '' s) = s :=
  e.toEquiv.preimage_image s
Preimage of Image under Order Isomorphism Equals Original Set
Informal description
For any order isomorphism $e : \alpha \simeq \beta$ between ordered types $\alpha$ and $\beta$, and any subset $s \subseteq \alpha$, the preimage of the image of $s$ under $e$ equals $s$ itself. In symbols, $e^{-1}(e(s)) = s$.
OrderIso.setCongr definition
(s t : Set α) (h : s = t) : s ≃o t
Full source 
/-- Order isomorphism between two equal sets. -/
def setCongr (s t : Set α) (h : s = t) :
    s ≃o t where
  toEquiv := Equiv.setCongr h
  map_rel_iff' := Iff.rfl
Order isomorphism between equal sets
Informal description
Given a type $\alpha$ and two subsets $s, t \subseteq \alpha$ that are equal ($s = t$), there exists an order isomorphism between the subtypes corresponding to $s$ and $t$. This isomorphism preserves the order structure, meaning for any $x, y \in s$, $x \leq y$ if and only if their images under the isomorphism satisfy the same relation in $t$.
OrderIso.Set.univ definition
: (Set.univ : Set α) ≃o α
Full source 
/-- Order isomorphism between `univ : Set α` and `α`. -/
def Set.univ : (Set.univ : Set α) ≃o α where
  toEquiv := Equiv.Set.univ α
  map_rel_iff' := Iff.rfl
Order isomorphism between universal set and base type
Informal description
The order isomorphism between the universal set `univ : Set α` and the type `α` itself, where the bijection is given by the natural equivalence and the order relation is preserved.
OrderEmbedding.orderIso definition
[LE α] [LE β] {f : α ↪o β} : α ≃o Set.range f
Full source 
/-- We can regard an order embedding as an order isomorphism to its range. -/
@[simps! apply]
noncomputable def OrderEmbedding.orderIso [LE α] [LE β] {f : α ↪o β} :
    α ≃o Set.range f :=
  { Equiv.ofInjective _ f.injective with
    map_rel_iff' := f.map_rel_iff }
Order isomorphism induced by an order embedding
Informal description
Given an order embedding $f : \alpha \hookrightarrow \beta$ between partially ordered sets $\alpha$ and $\beta$, there exists an order isomorphism between $\alpha$ and the range of $f$. The isomorphism maps each element $a \in \alpha$ to $f(a) \in \text{range}(f)$, and its inverse maps each element in the range back to its unique preimage in $\alpha$. Moreover, for any $a, b \in \alpha$, $a \leq b$ if and only if $f(a) \leq f(b)$.
StrictMonoOn.orderIso definition
{α β} [LinearOrder α] [Preorder β] (f : α → β) (s : Set α) (hf : StrictMonoOn f s) : s ≃o f '' s
Full source 
/-- If a function `f` is strictly monotone on a set `s`, then it defines an order isomorphism
between `s` and its image. -/
protected noncomputable def StrictMonoOn.orderIso {α β} [LinearOrder α] [Preorder β] (f : α → β)
    (s : Set α) (hf : StrictMonoOn f s) :
    s ≃o f '' s where
  toEquiv := hf.injOn.bijOn_image.equiv _
  map_rel_iff' := hf.le_iff_le (Subtype.property _) (Subtype.property _)
Order isomorphism induced by a strictly monotone function on a set
Informal description
Given a linearly ordered set $\alpha$, a preordered set $\beta$, a function $f : \alpha \to \beta$, and a subset $s \subseteq \alpha$, if $f$ is strictly monotone on $s$, then $f$ induces an order isomorphism between $s$ and its image $f '' s \subseteq \beta$.
StrictMono.orderIso definition
: α ≃o Set.range f
Full source 
/-- A strictly monotone function from a linear order is an order isomorphism between its domain and
its range. -/
@[simps! apply]
protected noncomputable def orderIso :
    α ≃o Set.range f where
  toEquiv := Equiv.ofInjective f h_mono.injective
  map_rel_iff' := h_mono.le_iff_le
Order isomorphism induced by a strictly monotone function
Informal description
Given a strictly monotone function \( f : \alpha \to \beta \) between a linearly ordered set \( \alpha \) and a preordered set \( \beta \), the function \( f \) induces an order isomorphism between \( \alpha \) and the range of \( f \). The isomorphism maps each \( a \in \alpha \) to \( f(a) \), and its inverse maps each \( b \) in the range of \( f \) back to the unique \( a \in \alpha \) such that \( f(a) = b \).
StrictMono.orderIsoOfSurjective definition
: α ≃o β
Full source 
/-- A strictly monotone surjective function from a linear order is an order isomorphism. -/
noncomputable def orderIsoOfSurjective : α ≃o β :=
  (h_mono.orderIso f).trans <|
    (OrderIso.setCongr _ _ h_surj.range_eq).trans OrderIso.Set.univ
Order isomorphism induced by a strictly monotone surjective function
Informal description
Given a strictly monotone and surjective function \( f : \alpha \to \beta \) between a linearly ordered set \( \alpha \) and a preordered set \( \beta \), there exists an order isomorphism between \( \alpha \) and \( \beta \). This isomorphism is constructed by first restricting \( f \) to an order isomorphism between \( \alpha \) and the range of \( f \), then using the surjectivity to identify the range with \( \beta \), and finally composing with the natural order isomorphism between the universal set and \( \beta \).
StrictMono.coe_orderIsoOfSurjective theorem
: (orderIsoOfSurjective f h_mono h_surj : α → β) = f
Full source 
@[simp]
theorem coe_orderIsoOfSurjective : (orderIsoOfSurjective f h_mono h_surj : α → β) = f :=
  rfl
Underlying Function of Order Isomorphism Induced by Strictly Monotone Surjective Function Equals Original Function
Informal description
For a strictly monotone and surjective function $f \colon \alpha \to \beta$ between a linearly ordered set $\alpha$ and a preordered set $\beta$, the underlying function of the order isomorphism $\text{orderIsoOfSurjective}\, f\, h_{\text{mono}}\, h_{\text{surj}}$ is equal to $f$.
StrictMono.orderIsoOfSurjective_symm_apply_self theorem
(a : α) : (orderIsoOfSurjective f h_mono h_surj).symm (f a) = a
Full source 
@[simp]
theorem orderIsoOfSurjective_symm_apply_self (a : α) :
    (orderIsoOfSurjective f h_mono h_surj).symm (f a) = a :=
  (orderIsoOfSurjective f h_mono h_surj).symm_apply_apply _
Inverse of Order Isomorphism Induced by Strictly Monotone Surjective Function Fixes Preimages
Informal description
Let $f : \alpha \to \beta$ be a strictly monotone and surjective function between a linearly ordered set $\alpha$ and a preordered set $\beta$. Then the inverse of the order isomorphism induced by $f$ satisfies $(f^{-1} \circ f)(a) = a$ for all $a \in \alpha$.
StrictMono.orderIsoOfSurjective_self_symm_apply theorem
(b : β) : f ((orderIsoOfSurjective f h_mono h_surj).symm b) = b
Full source 
theorem orderIsoOfSurjective_self_symm_apply (b : β) :
    f ((orderIsoOfSurjective f h_mono h_surj).symm b) = b :=
  (orderIsoOfSurjective f h_mono h_surj).apply_symm_apply _
Inverse Property of Strictly Monotone Surjective Order Isomorphism
Informal description
For any element $b$ in a preordered set $\beta$, if $f : \alpha \to \beta$ is a strictly monotone and surjective function from a linearly ordered set $\alpha$ to $\beta$, then applying $f$ to the inverse of the order isomorphism induced by $f$ at $b$ yields $b$ itself, i.e., $f(f^{-1}(b)) = b$.
OrderEmbedding.range_inj theorem
[LinearOrder α] [WellFoundedLT α] [Preorder β] {f g : α ↪o β} : Set.range f = Set.range g ↔ f = g
Full source 
/-- Two order embeddings on a well-order are equal provided that their ranges are equal. -/
lemma OrderEmbedding.range_inj [LinearOrder α] [WellFoundedLT α] [Preorder β] {f g : α ↪o β} :
    Set.rangeSet.range f = Set.range g ↔ f = g := by
  rw [f.strictMono.range_inj g.strictMono, DFunLike.coe_fn_eq]
Equality of Order Embeddings via Range Equality on Well-Ordered Domains
Informal description
Let $\alpha$ be a linear order with a well-founded strict order relation $<$, and let $\beta$ be a preorder. For any two order embeddings $f, g : \alpha \hookrightarrow \beta$, the ranges of $f$ and $g$ are equal if and only if $f = g$.
OrderIso.subsingleton_of_wellFoundedLT instance
[LinearOrder α] [WellFoundedLT α] [Preorder β] : Subsingleton (α ≃o β)
Full source 
instance subsingleton_of_wellFoundedLT [LinearOrder α] [WellFoundedLT α] [Preorder β] :
    Subsingleton (α ≃o β) := by
  refine ⟨fun f g ↦ ?_⟩
  rw [OrderIso.ext_iff, ← coe_toOrderEmbedding, ← coe_toOrderEmbedding, DFunLike.coe_fn_eq,
    ← OrderEmbedding.range_inj, coe_toOrderEmbedding, coe_toOrderEmbedding, range_eq, range_eq]
Uniqueness of Order Isomorphisms from Well-Founded Linear Orders
Informal description
For any linearly ordered type $\alpha$ with a well-founded less-than relation and any preordered type $\beta$, the type of order isomorphisms from $\alpha$ to $\beta$ is a subsingleton (i.e., has at most one element up to equality).
OrderIso.subsingleton_of_wellFoundedLT' instance
[LinearOrder β] [WellFoundedLT β] [Preorder α] : Subsingleton (α ≃o β)
Full source 
instance subsingleton_of_wellFoundedLT' [LinearOrder β] [WellFoundedLT β] [Preorder α] :
    Subsingleton (α ≃o β) := by
  refine ⟨fun f g ↦ ?_⟩
  change f.symm.symm = g.symm.symm
  rw [Subsingleton.elim f.symm]
Uniqueness of Order Isomorphisms to Well-Founded Linear Orders
Informal description
For any linearly ordered type $\beta$ with a well-founded less-than relation and any preordered type $\alpha$, the type of order isomorphisms from $\alpha$ to $\beta$ is a subsingleton (i.e., has at most one element up to equality).
OrderIso.unique_of_wellFoundedLT instance
[LinearOrder α] [WellFoundedLT α] : Unique (α ≃o α)
Full source 
instance unique_of_wellFoundedLT [LinearOrder α] [WellFoundedLT α] : Unique (α ≃o α) := Unique.mk' _
Uniqueness of Identity Order Isomorphism for Well-Founded Linear Orders
Informal description
For any linearly ordered type $\alpha$ with a well-founded less-than relation, there is exactly one order isomorphism from $\alpha$ to itself (the identity map).
OrderIso.subsingleton_of_wellFoundedGT instance
[LinearOrder α] [WellFoundedGT α] [Preorder β] : Subsingleton (α ≃o β)
Full source 
instance subsingleton_of_wellFoundedGT [LinearOrder α] [WellFoundedGT α] [Preorder β] :
    Subsingleton (α ≃o β) := by
  refine ⟨fun f g ↦ ?_⟩
  change f.dual.dual = g.dual.dual
  rw [Subsingleton.elim f.dual]
Uniqueness of Order Isomorphisms from Well-Founded Linear Orders with Well-Founded Greater-Than Relation
Informal description
For any linearly ordered type $\alpha$ with a well-founded greater-than relation and any preordered type $\beta$, the type of order isomorphisms from $\alpha$ to $\beta$ is a subsingleton (i.e., has at most one element up to equality).
OrderIso.subsingleton_of_wellFoundedGT' instance
[LinearOrder β] [WellFoundedGT β] [Preorder α] : Subsingleton (α ≃o β)
Full source 
instance subsingleton_of_wellFoundedGT' [LinearOrder β] [WellFoundedGT β] [Preorder α] :
    Subsingleton (α ≃o β) := by
  refine ⟨fun f g ↦ ?_⟩
  change f.dual.dual = g.dual.dual
  rw [Subsingleton.elim f.dual]
Uniqueness of Order Isomorphisms to Well-Founded Linear Orders with Well-Founded Greater-Than Relation
Informal description
For any linearly ordered type $\beta$ with a well-founded greater-than relation and any preordered type $\alpha$, the type of order isomorphisms from $\alpha$ to $\beta$ is a subsingleton (i.e., has at most one element up to equality).
OrderIso.unique_of_wellFoundedGT instance
[LinearOrder α] [WellFoundedGT α] : Unique (α ≃o α)
Full source 
instance unique_of_wellFoundedGT [LinearOrder α] [WellFoundedGT α] : Unique (α ≃o α) := Unique.mk' _
Uniqueness of Order Isomorphism on Well-Founded Linear Orders
Informal description
For any linearly ordered type $\alpha$ with a well-founded greater-than relation, there is exactly one order isomorphism from $\alpha$ to itself (the identity map).
OrderIso.Iic definition
[Lattice α] [Lattice β] (e : α ≃o β) (x : α) : Iic x ≃o Iic (e x)
Full source 
/-- An order isomorphism between lattices induces an order isomorphism between corresponding
interval sublattices. -/
protected def Iic [Lattice α] [Lattice β] (e : α ≃o β) (x : α) :
    IicIic x ≃o Iic (e x) where
  toFun y := ⟨e y, (map_le_map_iff _).mpr y.property⟩
  invFun y := ⟨e.symm y, e.symm_apply_le.mpr y.property⟩
  left_inv y := by simp
  right_inv y := by simp
  map_rel_iff' := by simp
Order isomorphism between interval sublattices $(-\infty, x]$ and $(-\infty, e(x)]$
Informal description
Given a lattice isomorphism $e : \alpha \simeq \beta$ between lattices $\alpha$ and $\beta$, and an element $x \in \alpha$, the map $e$ induces an order isomorphism between the interval sublattices $(-\infty, x] \subseteq \alpha$ and $(-\infty, e(x)] \subseteq \beta$. Specifically, the isomorphism maps each $y \in (-\infty, x]$ to $e(y) \in (-\infty, e(x)]$, and its inverse maps each $z \in (-\infty, e(x)]$ back to $e^{-1}(z) \in (-\infty, x]$.
OrderIso.Ici definition
[Lattice α] [Lattice β] (e : α ≃o β) (x : α) : Ici x ≃o Ici (e x)
Full source 
/-- An order isomorphism between lattices induces an order isomorphism between corresponding
interval sublattices. -/
protected def Ici [Lattice α] [Lattice β] (e : α ≃o β) (x : α) :
    IciIci x ≃o Ici (e x) where
  toFun y := ⟨e y, (map_le_map_iff _).mpr y.property⟩
  invFun y := ⟨e.symm y, e.le_symm_apply.mpr y.property⟩
  left_inv y := by simp
  right_inv y := by simp
  map_rel_iff' := by simp
Order isomorphism between upper intervals induced by a lattice isomorphism
Informal description
Given a lattice isomorphism $e : \alpha \simeq \beta$ between lattices $\alpha$ and $\beta$, and an element $x \in \alpha$, the map $e$ induces an order isomorphism between the intervals $[x, \infty)$ in $\alpha$ and $[e(x), \infty)$ in $\beta$. Specifically, the isomorphism maps each $y \in [x, \infty)$ to $e(y) \in [e(x), \infty)$, and its inverse maps each $z \in [e(x), \infty)$ back to $e^{-1}(z) \in [x, \infty)$.
OrderIso.Icc definition
[Lattice α] [Lattice β] (e : α ≃o β) (x y : α) : Icc x y ≃o Icc (e x) (e y)
Full source 
/-- An order isomorphism between lattices induces an order isomorphism between corresponding
interval sublattices. -/
protected def Icc [Lattice α] [Lattice β] (e : α ≃o β) (x y : α) :
    IccIcc x y ≃o Icc (e x) (e y) where
  toFun z := ⟨e z, by simp only [mem_Icc, map_le_map_iff]; exact z.property⟩
  invFun z := ⟨e.symm z, by simp only [mem_Icc, e.le_symm_apply, e.symm_apply_le]; exact z.property⟩
  left_inv y := by simp
  right_inv y := by simp
  map_rel_iff' := by simp
Order isomorphism between closed intervals induced by a lattice isomorphism
Informal description
Given two lattices $\alpha$ and $\beta$ and an order isomorphism $e : \alpha \simeq \beta$, the function maps any closed interval $[x, y]$ in $\alpha$ to the corresponding closed interval $[e(x), e(y)]$ in $\beta$ via $e$, and this mapping is itself an order isomorphism between the intervals.
OrderIso.compl definition
: α ≃o αᵒᵈ
Full source 
/-- Taking complements as an order isomorphism to the order dual. -/
@[simps!]
def OrderIso.compl : α ≃o αᵒᵈ where
  toFun := OrderDual.toDualOrderDual.toDual ∘ HasCompl.compl
  invFun := HasCompl.complHasCompl.compl ∘ OrderDual.ofDual
  left_inv := compl_compl
  right_inv := compl_compl (α := αᵒᵈ)
  map_rel_iff' := compl_le_compl_iff_le
Order isomorphism between a lattice and its order dual via complements
Informal description
The order isomorphism `OrderIso.compl` maps an element of a lattice $\alpha$ to its complement in the order dual lattice $\alpha^{\text{op}}$. It is defined by composing the complement operation with the order dual isomorphism, and satisfies the property that applying the complement operation twice returns the original element. The isomorphism preserves the order relation in the sense that for any two elements $x, y \in \alpha$, the complement of $x$ is less than or equal to the complement of $y$ in the dual order if and only if $y \leq x$ in the original order.
compl_strictAnti theorem
: StrictAnti (compl : α → α)
Full source 
theorem compl_strictAnti : StrictAnti (compl : α → α) :=
  (OrderIso.compl α).strictMono
Strict Antitonicity of Lattice Complement Operation
Informal description
The complement operation $\text{compl} : \alpha \to \alpha$ on a lattice $\alpha$ is strictly antitone, meaning that for any $x, y \in \alpha$, if $x < y$ then $\text{compl}(y) < \text{compl}(x)$.
compl_antitone theorem
: Antitone (compl : α → α)
Full source 
theorem compl_antitone : Antitone (compl : α → α) :=
  (OrderIso.compl α).monotone
Antitonicity of Lattice Complement Operation
Informal description
The complement operation on a lattice $\alpha$ is antitone, meaning that for any $x, y \in \alpha$, if $x \leq y$ then $\text{compl}(y) \leq \text{compl}(x)$.