Module docstring
{"# Lemmas about images of intervals under order isomorphisms. "}
OrderIso.preimage_Iic
theorem
(e : α ≃o β) (b : β) : e ⁻¹' Iic b = Iic (e.symm b)
Full source
@[simp]
theorem preimage_Iic (e : α ≃o β) (b : β) : e ⁻¹' Iic b = Iic (e.symm b) := by
ext x
simp [← e.le_iff_le]Informal description
Let $e : \alpha \simeq \beta$ be an order isomorphism between preorders $\alpha$ and $\beta$. For any element $b \in \beta$, the preimage of the left-infinite right-closed interval $(-\infty, b]$ under $e$ is equal to the left-infinite right-closed interval $(-\infty, e^{-1}(b)]$ in $\alpha$. That is,
$$ e^{-1}((-\infty, b]) = (-\infty, e^{-1}(b)]. $$
OrderIso.preimage_Ici
theorem
(e : α ≃o β) (b : β) : e ⁻¹' Ici b = Ici (e.symm b)
Full source
@[simp]
theorem preimage_Ici (e : α ≃o β) (b : β) : e ⁻¹' Ici b = Ici (e.symm b) := by
ext x
simp [← e.le_iff_le]Informal description
Let $e : \alpha \simeq \beta$ be an order isomorphism between two preorders $\alpha$ and $\beta$. For any element $b \in \beta$, the preimage of the left-closed right-infinite interval $[b, \infty)$ under $e$ is equal to the left-closed right-infinite interval $[e^{-1}(b), \infty)$ in $\alpha$. That is,
$$ e^{-1}([b, \infty)) = [e^{-1}(b), \infty). $$
OrderIso.preimage_Iio
theorem
(e : α ≃o β) (b : β) : e ⁻¹' Iio b = Iio (e.symm b)
Full source
@[simp]
theorem preimage_Iio (e : α ≃o β) (b : β) : e ⁻¹' Iio b = Iio (e.symm b) := by
ext x
simp [← e.lt_iff_lt]Informal description
Let $e : \alpha \simeq \beta$ be an order isomorphism between two preorders $\alpha$ and $\beta$. For any element $b \in \beta$, the preimage of the left-infinite right-open interval $(-\infty, b)$ under $e$ is equal to the left-infinite right-open interval $(-\infty, e^{-1}(b))$ in $\alpha$. In other words:
$$ e^{-1}\big( (-\infty, b) \big) = (-\infty, e^{-1}(b)) $$
OrderIso.preimage_Ioi
theorem
(e : α ≃o β) (b : β) : e ⁻¹' Ioi b = Ioi (e.symm b)
Full source
@[simp]
theorem preimage_Ioi (e : α ≃o β) (b : β) : e ⁻¹' Ioi b = Ioi (e.symm b) := by
ext x
simp [← e.lt_iff_lt]Informal description
For an order isomorphism $e : \alpha \simeq \beta$ and an element $b \in \beta$, the preimage of the left-open right-infinite interval $(b, \infty)$ under $e$ is equal to the left-open right-infinite interval $(e^{-1}(b), \infty)$ in $\alpha$, i.e.,
$$ e^{-1}((b, \infty)) = (e^{-1}(b), \infty). $$
OrderIso.preimage_Icc
theorem
(e : α ≃o β) (a b : β) : e ⁻¹' Icc a b = Icc (e.symm a) (e.symm b)
Full source
@[simp]
theorem preimage_Icc (e : α ≃o β) (a b : β) : e ⁻¹' Icc a b = Icc (e.symm a) (e.symm b) := by
simp [← Ici_inter_Iic]Informal description
Let $e : \alpha \simeq \beta$ be an order isomorphism between two preorders $\alpha$ and $\beta$. For any elements $a, b \in \beta$, the preimage of the closed interval $[a, b]$ under $e$ is equal to the closed interval $[e^{-1}(a), e^{-1}(b)]$ in $\alpha$. That is,
$$ e^{-1}([a, b]) = [e^{-1}(a), e^{-1}(b)]. $$
OrderIso.preimage_Ico
theorem
(e : α ≃o β) (a b : β) : e ⁻¹' Ico a b = Ico (e.symm a) (e.symm b)
Full source
@[simp]
theorem preimage_Ico (e : α ≃o β) (a b : β) : e ⁻¹' Ico a b = Ico (e.symm a) (e.symm b) := by
simp [← Ici_inter_Iio]Informal description
Let $e : \alpha \simeq \beta$ be an order isomorphism between two preorders $\alpha$ and $\beta$. For any elements $a, b \in \beta$, the preimage of the left-closed right-open interval $[a, b)$ under $e$ is equal to the left-closed right-open interval $[e^{-1}(a), e^{-1}(b))$ in $\alpha$. That is,
$$ e^{-1}([a, b)) = [e^{-1}(a), e^{-1}(b)). $$
OrderIso.preimage_Ioc
theorem
(e : α ≃o β) (a b : β) : e ⁻¹' Ioc a b = Ioc (e.symm a) (e.symm b)
Full source
@[simp]
theorem preimage_Ioc (e : α ≃o β) (a b : β) : e ⁻¹' Ioc a b = Ioc (e.symm a) (e.symm b) := by
simp [← Ioi_inter_Iic]Informal description
Let $e : \alpha \simeq \beta$ be an order isomorphism between preorders $\alpha$ and $\beta$. For any elements $a, b \in \beta$, the preimage of the left-open right-closed interval $(a, b]$ under $e$ is equal to the left-open right-closed interval $(e^{-1}(a), e^{-1}(b)]$ in $\alpha$. That is,
$$ e^{-1}((a, b]) = (e^{-1}(a), e^{-1}(b)]. $$
OrderIso.preimage_Ioo
theorem
(e : α ≃o β) (a b : β) : e ⁻¹' Ioo a b = Ioo (e.symm a) (e.symm b)
Full source
@[simp]
theorem preimage_Ioo (e : α ≃o β) (a b : β) : e ⁻¹' Ioo a b = Ioo (e.symm a) (e.symm b) := by
simp [← Ioi_inter_Iio]Informal description
Let $e : \alpha \simeqo \beta$ be an order isomorphism between two preorders $\alpha$ and $\beta$. For any elements $a, b \in \beta$, the preimage of the open interval $(a, b)$ under $e$ is equal to the open interval $(e^{-1}(a), e^{-1}(b))$ in $\alpha$, i.e.,
$$ e^{-1}\big( (a, b) \big) = (e^{-1}(a), e^{-1}(b)). $$
OrderIso.image_Iic
theorem
(e : α ≃o β) (a : α) : e '' Iic a = Iic (e a)
Full source
@[simp]
theorem image_Iic (e : α ≃o β) (a : α) : e '' Iic a = Iic (e a) := by
rw [e.image_eq_preimage, e.symm.preimage_Iic, e.symm_symm]Informal description
Let $e : \alpha \simeqo \beta$ be an order isomorphism between preorders $\alpha$ and $\beta$. For any element $a \in \alpha$, the image of the left-infinite right-closed interval $(-\infty, a]$ under $e$ is equal to the left-infinite right-closed interval $(-\infty, e(a)]$ in $\beta$. That is,
$$ e\big( (-\infty, a] \big) = (-\infty, e(a)]. $$
OrderIso.image_Ici
theorem
(e : α ≃o β) (a : α) : e '' Ici a = Ici (e a)
Informal description
Let $e : \alpha \simeqo \beta$ be an order isomorphism between preorders $\alpha$ and $\beta$. For any element $a \in \alpha$, the image of the left-closed right-infinite interval $[a, \infty)$ under $e$ is equal to the left-closed right-infinite interval $[e(a), \infty)$ in $\beta$. That is,
$$ e\big( [a, \infty) \big) = [e(a), \infty). $$
OrderIso.image_Iio
theorem
(e : α ≃o β) (a : α) : e '' Iio a = Iio (e a)
Full source
@[simp]
theorem image_Iio (e : α ≃o β) (a : α) : e '' Iio a = Iio (e a) := by
rw [e.image_eq_preimage, e.symm.preimage_Iio, e.symm_symm]Informal description
Let $e : \alpha \simeq \beta$ be an order isomorphism between two preorders $\alpha$ and $\beta$. For any element $a \in \alpha$, the image of the left-infinite right-open interval $(-\infty, a)$ under $e$ is equal to the left-infinite right-open interval $(-\infty, e(a))$ in $\beta$. In other words:
$$ e\big( (-\infty, a) \big) = (-\infty, e(a)) $$
OrderIso.image_Ioi
theorem
(e : α ≃o β) (a : α) : e '' Ioi a = Ioi (e a)
Informal description
Let $e : \alpha \simeq \beta$ be an order isomorphism between two preorders $\alpha$ and $\beta$. For any element $a \in \alpha$, the image of the left-open right-infinite interval $(a, \infty)$ under $e$ is equal to the left-open right-infinite interval $(e(a), \infty)$ in $\beta$. In other words:
$$ e\big( (a, \infty) \big) = (e(a), \infty) $$
OrderIso.image_Ioo
theorem
(e : α ≃o β) (a b : α) : e '' Ioo a b = Ioo (e a) (e b)
Full source
@[simp]
theorem image_Ioo (e : α ≃o β) (a b : α) : e '' Ioo a b = Ioo (e a) (e b) := by
rw [e.image_eq_preimage, e.symm.preimage_Ioo, e.symm_symm]Informal description
Let $e : \alpha \simeqo \beta$ be an order isomorphism between two preorders $\alpha$ and $\beta$. For any elements $a, b \in \alpha$, the image of the open interval $(a, b)$ under $e$ is equal to the open interval $(e(a), e(b))$ in $\beta$, i.e.,
$$ e\big( (a, b) \big) = (e(a), e(b)). $$
OrderIso.image_Ioc
theorem
(e : α ≃o β) (a b : α) : e '' Ioc a b = Ioc (e a) (e b)
Full source
@[simp]
theorem image_Ioc (e : α ≃o β) (a b : α) : e '' Ioc a b = Ioc (e a) (e b) := by
rw [e.image_eq_preimage, e.symm.preimage_Ioc, e.symm_symm]Informal description
Let $e : \alpha \simeq \beta$ be an order isomorphism between preorders $\alpha$ and $\beta$. For any elements $a, b \in \alpha$, the image of the left-open right-closed interval $(a, b]$ under $e$ is equal to the left-open right-closed interval $(e(a), e(b)]$ in $\beta$. That is,
$$ e((a, b]) = (e(a), e(b)]. $$
OrderIso.image_Ico
theorem
(e : α ≃o β) (a b : α) : e '' Ico a b = Ico (e a) (e b)
Full source
@[simp]
theorem image_Ico (e : α ≃o β) (a b : α) : e '' Ico a b = Ico (e a) (e b) := by
rw [e.image_eq_preimage, e.symm.preimage_Ico, e.symm_symm]Informal description
Let $e : \alpha \simeq \beta$ be an order isomorphism between two preorders $\alpha$ and $\beta$. For any elements $a, b \in \alpha$, the image of the left-closed right-open interval $[a, b)$ under $e$ is equal to the left-closed right-open interval $[e(a), e(b))$ in $\beta$. That is,
$$ e([a, b)) = [e(a), e(b)). $$
OrderIso.image_Icc
theorem
(e : α ≃o β) (a b : α) : e '' Icc a b = Icc (e a) (e b)
Full source
@[simp]
theorem image_Icc (e : α ≃o β) (a b : α) : e '' Icc a b = Icc (e a) (e b) := by
rw [e.image_eq_preimage, e.symm.preimage_Icc, e.symm_symm]Informal description
Let $e : \alpha \simeq \beta$ be an order isomorphism between two preorders $\alpha$ and $\beta$. For any elements $a, b \in \alpha$, the image of the closed interval $[a, b]$ under $e$ is equal to the closed interval $[e(a), e(b)]$ in $\beta$. That is,
$$ e([a, b]) = [e(a), e(b)]. $$
OrderIso.IicTop
definition
{α : Type*} [Preorder α] [OrderTop α] : Iic (⊤ : α) ≃o α
Full source
/-- Order isomorphism between `Iic (⊤ : α)` and `α` when `α` has a top element -/
def IicTop {α : Type*} [Preorder α] [OrderTop α] : IicIic (⊤ : α) ≃o α :=
{ @Equiv.subtypeUnivEquiv α (Iic (⊤ : α)) fun _ => le_top with
map_rel_iff' := @fun x y => by rfl }Informal description
Given a preorder $\alpha$ with a top element $\top$, the order isomorphism $\text{Iic}(\top) \simeq \alpha$ maps the left-infinite right-closed interval $(-\infty, \top]$ to the entire type $\alpha$.
OrderIso.IciBot
definition
{α : Type*} [Preorder α] [OrderBot α] : Ici (⊥ : α) ≃o α
Full source
/-- Order isomorphism between `Ici (⊥ : α)` and `α` when `α` has a bottom element -/
def IciBot {α : Type*} [Preorder α] [OrderBot α] : IciIci (⊥ : α) ≃o α :=
{ @Equiv.subtypeUnivEquiv α (Ici (⊥ : α)) fun _ => bot_le with
map_rel_iff' := @fun x y => by rfl }Informal description
Given a preorder $\alpha$ with a bottom element $\bot$, the order isomorphism $\text{Ici}(\bot) \simeq \alpha$ maps the left-closed right-infinite interval $[\bot, \infty)$ to the entire type $\alpha$.