Mathlib.Order.Interval.Set.WithBotTop

WithTop.preimage_coe_top theorem

: (some : α → WithTop α) ⁻¹' {⊤} = (∅ : Set α)

Full source

@[simp]
theorem preimage_coe_top : (some : α → WithTop α) ⁻¹' {⊤} = (∅ : Set α) :=
  eq_empty_of_subset_empty fun _ => coe_ne_top

Preimage of Top in WithTop is Empty

Informal description

The preimage of the singleton set $\{\top\}$ under the canonical embedding $\text{some} : \alpha \to \text{WithTop} \alpha$ is the empty set, i.e., $\text{some}^{-1}(\{\top\}) = \emptyset$.

WithTop.range_coe theorem

: range (some : α → WithTop α) = Iio ⊤

Full source

theorem range_coe : range (some : α → WithTop α) = Iio ⊤ := by
  ext x
  rw [mem_Iio, WithTop.lt_top_iff_ne_top, mem_range, ne_top_iff_exists]

Range of Canonical Embedding in $\text{WithTop} \alpha$ is $(-\infty, \top)$

Informal description

The range of the canonical embedding $\text{some} : \alpha \to \text{WithTop} \alpha$ is equal to the left-infinite right-open interval $(-\infty, \top)$ in $\text{WithTop} \alpha$, i.e., $\text{range}(\text{some}) = (-\infty, \top)$.

WithTop.preimage_coe_Ioi theorem

: (some : α → WithTop α) ⁻¹' Ioi a = Ioi a

Full source

@[simp]
theorem preimage_coe_Ioi : (some : α → WithTop α) ⁻¹' Ioi a = Ioi a :=
  ext fun _ => coe_lt_coe

Preimage of Ioi under WithTop Embedding Equals Ioi

Informal description

For any element $a$ in a preorder $\alpha$, the preimage of the left-open right-infinite interval $(a, \infty)$ under the canonical embedding $\text{some} : \alpha \to \text{WithTop} \alpha$ is equal to the interval $(a, \infty)$ in $\alpha$, i.e., $\text{some}^{-1}((a, \infty)) = (a, \infty)$.

WithTop.preimage_coe_Ici theorem

: (some : α → WithTop α) ⁻¹' Ici a = Ici a

Full source

@[simp]
theorem preimage_coe_Ici : (some : α → WithTop α) ⁻¹' Ici a = Ici a :=
  ext fun _ => coe_le_coe

Preimage of $[a, \infty)$ under canonical embedding to $\text{WithTop} \alpha$ equals $[a, \infty)$ in $\alpha$

Informal description

For any element $a$ in a preorder $\alpha$, the preimage of the left-closed right-infinite interval $[a, \infty)$ under the canonical embedding $\text{some} : \alpha \to \text{WithTop} \alpha$ is equal to $[a, \infty)$ in $\alpha$.

WithTop.preimage_coe_Iio theorem

: (some : α → WithTop α) ⁻¹' Iio a = Iio a

Full source

@[simp]
theorem preimage_coe_Iio : (some : α → WithTop α) ⁻¹' Iio a = Iio a :=
  ext fun _ => coe_lt_coe

Preimage of $(-\infty, a)$ under $\operatorname{some}$ embedding equals $(-\infty, a)$

Informal description

For any element $a$ in a preorder $\alpha$, the preimage of the left-infinite right-open interval $(-\infty, a)$ under the canonical embedding $\operatorname{some} : \alpha \to \operatorname{WithTop} \alpha$ is equal to the interval $(-\infty, a)$ itself. In other words, $\operatorname{some}^{-1}((-\infty, a)) = (-\infty, a)$.

WithTop.preimage_coe_Iic theorem

: (some : α → WithTop α) ⁻¹' Iic a = Iic a

Full source

@[simp]
theorem preimage_coe_Iic : (some : α → WithTop α) ⁻¹' Iic a = Iic a :=
  ext fun _ => coe_le_coe

Preimage of $(-\infty, a]$ under $\text{some} : \alpha \to \text{WithTop} \alpha$ equals $(-\infty, a]$ in $\alpha$

Informal description

For any element $a$ in a preorder $\alpha$, the preimage of the left-infinite right-closed interval $(-\infty, a]$ under the canonical embedding $\text{some} : \alpha \to \text{WithTop} \alpha$ is equal to the interval $(-\infty, a]$ in $\alpha$.

WithTop.preimage_coe_Icc theorem

: (some : α → WithTop α) ⁻¹' Icc a b = Icc a b

Full source

@[simp]
theorem preimage_coe_Icc : (some : α → WithTop α) ⁻¹' Icc a b = Icc a b := by simp [← Ici_inter_Iic]

Preimage of Closed Interval under Canonical Embedding to $\text{WithTop} \alpha$ Equals Closed Interval in $\alpha$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the preimage of the closed interval $[a, b]$ under the canonical embedding $\text{some} : \alpha \to \text{WithTop} \alpha$ is equal to the interval $[a, b]$ in $\alpha$. That is, $\text{some}^{-1}([a, b]) = [a, b]$.

WithTop.preimage_coe_Ico theorem

: (some : α → WithTop α) ⁻¹' Ico a b = Ico a b

Full source

@[simp]
theorem preimage_coe_Ico : (some : α → WithTop α) ⁻¹' Ico a b = Ico a b := by simp [← Ici_inter_Iio]

Preimage of $[a, b)$ under $\text{some}$ embedding equals $[a, b)$ in $\alpha$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the preimage of the left-closed right-open interval $[a, b)$ under the canonical embedding $\text{some} : \alpha \to \text{WithTop} \alpha$ is equal to the interval $[a, b)$ in $\alpha$. That is, $\text{some}^{-1}([a, b)) = [a, b)$.

WithTop.preimage_coe_Ioc theorem

: (some : α → WithTop α) ⁻¹' Ioc a b = Ioc a b

Full source

@[simp]
theorem preimage_coe_Ioc : (some : α → WithTop α) ⁻¹' Ioc a b = Ioc a b := by simp [← Ioi_inter_Iic]

Preimage of $(a, b]$ under $\text{some}$ embedding equals $(a, b]$ in $\alpha$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the preimage of the left-open right-closed interval $(a, b]$ under the canonical embedding $\text{some} : \alpha \to \text{WithTop} \alpha$ is equal to the interval $(a, b]$ in $\alpha$. That is, $\text{some}^{-1}((a, b]) = (a, b]$.

WithTop.preimage_coe_Ioo theorem

: (some : α → WithTop α) ⁻¹' Ioo a b = Ioo a b

Full source

@[simp]
theorem preimage_coe_Ioo : (some : α → WithTop α) ⁻¹' Ioo a b = Ioo a b := by simp [← Ioi_inter_Iio]

Preimage of Open Interval under WithTop Embedding Equals Open Interval

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the preimage of the open interval $(a, b)$ under the canonical embedding $\operatorname{some} : \alpha \to \operatorname{WithTop} \alpha$ is equal to the open interval $(a, b)$ in $\alpha$. That is, $\operatorname{some}^{-1}((a, b)) = (a, b)$.

WithTop.preimage_coe_Iio_top theorem

: (some : α → WithTop α) ⁻¹' Iio ⊤ = univ

Full source

@[simp]
theorem preimage_coe_Iio_top : (some : α → WithTop α) ⁻¹' Iio ⊤ = univ := by
  rw [← range_coe, preimage_range]

Preimage of $(-\infty, \top)$ under $\text{some}$ is the universal set

Informal description

For any type $\alpha$ with a preorder, the preimage of the left-infinite right-open interval $(-\infty, \top)$ under the canonical embedding $\text{some} : \alpha \to \text{WithTop} \alpha$ is the entire set $\alpha$. That is, $\text{some}^{-1}((-\infty, \top)) = \alpha$.

WithTop.preimage_coe_Ico_top theorem

: (some : α → WithTop α) ⁻¹' Ico a ⊤ = Ici a

Full source

@[simp]
theorem preimage_coe_Ico_top : (some : α → WithTop α) ⁻¹' Ico a ⊤ = Ici a := by
  simp [← Ici_inter_Iio]

Preimage of $[a, \top)$ under WithTop Embedding Equals $[a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$, the preimage of the left-closed right-open interval $[a, \top)$ under the canonical embedding $\text{some} : \alpha \to \text{WithTop} \alpha$ is equal to the left-closed right-infinite interval $[a, \infty)$ in $\alpha$. That is, $\text{some}^{-1}([a, \top)) = [a, \infty)$.

WithTop.preimage_coe_Ioo_top theorem

: (some : α → WithTop α) ⁻¹' Ioo a ⊤ = Ioi a

Full source

@[simp]
theorem preimage_coe_Ioo_top : (some : α → WithTop α) ⁻¹' Ioo a ⊤ = Ioi a := by
  simp [← Ioi_inter_Iio]

Preimage of $(a, \top)$ under $\text{some}$ equals $(a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$, the preimage of the open interval $(a, \top)$ under the canonical embedding $\text{some} : \alpha \to \text{WithTop} \alpha$ is equal to the left-open right-infinite interval $(a, \infty)$ in $\alpha$. That is, $\text{some}^{-1}((a, \top)) = (a, \infty)$.

WithTop.image_coe_Ioi theorem

: (some : α → WithTop α) '' Ioi a = Ioo (a : WithTop α) ⊤

Full source

theorem image_coe_Ioi : (some : α → WithTop α) '' Ioi a = Ioo (a : WithTop α) ⊤ := by
  rw [← preimage_coe_Ioi, image_preimage_eq_inter_range, range_coe, Ioi_inter_Iio]

Image of Right-Infinite Interval under WithTop Embedding Equals Open Interval to Top

Informal description

For any element $a$ in a preorder $\alpha$, the image of the left-open right-infinite interval $(a, \infty)$ under the canonical embedding $\text{some} : \alpha \to \text{WithTop} \alpha$ is equal to the open interval $(a, \top)$ in $\text{WithTop} \alpha$, i.e., $\text{some}((a, \infty)) = (a, \top)$.

WithTop.image_coe_Ici theorem

: (some : α → WithTop α) '' Ici a = Ico (a : WithTop α) ⊤

Full source

theorem image_coe_Ici : (some : α → WithTop α) '' Ici a = Ico (a : WithTop α) ⊤ := by
  rw [← preimage_coe_Ici, image_preimage_eq_inter_range, range_coe, Ici_inter_Iio]

Image of $[a, \infty)$ under canonical embedding to $\text{WithTop} \alpha$ equals $[a, \top)$

Informal description

For any element $a$ in a preorder $\alpha$, the image of the left-closed right-infinite interval $[a, \infty)$ under the canonical embedding $\text{some} : \alpha \to \text{WithTop} \alpha$ is equal to the left-closed right-open interval $[a, \top)$ in $\text{WithTop} \alpha$.

WithTop.image_coe_Iio theorem

: (some : α → WithTop α) '' Iio a = Iio (a : WithTop α)

Full source

theorem image_coe_Iio : (some : α → WithTop α) '' Iio a = Iio (a : WithTop α) := by
  rw [← preimage_coe_Iio, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Iio_subset_Iio le_top)]

Image of $(-\infty, a)$ under $\operatorname{some}$ embedding equals $(-\infty, a)$ in $\operatorname{WithTop} \alpha$

Informal description

For any element $a$ in a preorder $\alpha$, the image of the left-infinite right-open interval $(-\infty, a)$ under the canonical embedding $\operatorname{some} : \alpha \to \operatorname{WithTop} \alpha$ is equal to the interval $(-\infty, a)$ in $\operatorname{WithTop} \alpha$, i.e., $\operatorname{some}((-\infty, a)) = (-\infty, a)$.

WithTop.image_coe_Iic theorem

: (some : α → WithTop α) '' Iic a = Iic (a : WithTop α)

Full source

theorem image_coe_Iic : (some : α → WithTop α) '' Iic a = Iic (a : WithTop α) := by
  rw [← preimage_coe_Iic, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Iic_subset_Iio.2 <| coe_lt_top a)]

Image of $(-\infty, a]$ under $\text{some} : \alpha \to \text{WithTop} \alpha$ equals $(-\infty, a]$ in $\text{WithTop} \alpha$

Informal description

For any element $a$ in a preorder $\alpha$, the image of the left-infinite right-closed interval $(-\infty, a]$ under the canonical embedding $\text{some} : \alpha \to \text{WithTop} \alpha$ is equal to the interval $(-\infty, a]$ in $\text{WithTop} \alpha$.

WithTop.image_coe_Icc theorem

: (some : α → WithTop α) '' Icc a b = Icc (a : WithTop α) b

Full source

theorem image_coe_Icc : (some : α → WithTop α) '' Icc a b = Icc (a : WithTop α) b := by
  rw [← preimage_coe_Icc, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left
      (Subset.trans Icc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]

Image of Closed Interval under Canonical Embedding to $\text{WithTop} \alpha$ Equals Closed Interval in $\text{WithTop} \alpha$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the image of the closed interval $[a, b]$ under the canonical embedding $\text{some} : \alpha \to \text{WithTop} \alpha$ is equal to the closed interval $[a, b]$ in $\text{WithTop} \alpha$.

WithTop.image_coe_Ico theorem

: (some : α → WithTop α) '' Ico a b = Ico (a : WithTop α) b

Full source

theorem image_coe_Ico : (some : α → WithTop α) '' Ico a b = Ico (a : WithTop α) b := by
  rw [← preimage_coe_Ico, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Subset.trans Ico_subset_Iio_self <| Iio_subset_Iio le_top)]

Image of $[a, b)$ under $\text{some}$ equals $[a, b)$ in $\text{WithTop} \alpha$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the image of the left-closed right-open interval $[a, b)$ under the canonical embedding $\text{some} : \alpha \to \text{WithTop} \alpha$ is equal to the left-closed right-open interval $[a, b)$ in $\text{WithTop} \alpha$.

WithTop.image_coe_Ioc theorem

: (some : α → WithTop α) '' Ioc a b = Ioc (a : WithTop α) b

Full source

theorem image_coe_Ioc : (some : α → WithTop α) '' Ioc a b = Ioc (a : WithTop α) b := by
  rw [← preimage_coe_Ioc, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left
      (Subset.trans Ioc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]

Image of $(a, b]$ under $\text{some}$ equals $(a, b]$ in $\text{WithTop} \alpha$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the image of the left-open right-closed interval $(a, b]$ under the canonical embedding $\text{some} : \alpha \to \text{WithTop} \alpha$ is equal to the left-open right-closed interval $(a, b]$ in $\text{WithTop} \alpha$.

WithTop.image_coe_Ioo theorem

: (some : α → WithTop α) '' Ioo a b = Ioo (a : WithTop α) b

Full source

theorem image_coe_Ioo : (some : α → WithTop α) '' Ioo a b = Ioo (a : WithTop α) b := by
  rw [← preimage_coe_Ioo, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Subset.trans Ioo_subset_Iio_self <| Iio_subset_Iio le_top)]

Image of Open Interval under Canonical Embedding in $\operatorname{WithTop} \alpha$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the image of the open interval $(a, b)$ under the canonical embedding $\operatorname{some} : \alpha \to \operatorname{WithTop} \alpha$ is equal to the open interval $(a, b)$ in $\operatorname{WithTop} \alpha$. That is, $\operatorname{some}((a, b)) = (a, b)$.

WithBot.preimage_coe_bot theorem

: (some : α → WithBot α) ⁻¹' {⊥} = (∅ : Set α)

Full source

@[simp]
theorem preimage_coe_bot : (some : α → WithBot α) ⁻¹' {⊥} = (∅ : Set α) :=
  @WithTop.preimage_coe_top αᵒᵈ

Preimage of Bottom in WithBot is Empty

Informal description

The preimage of the singleton set $\{\bot\}$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot} \alpha$ is the empty set, i.e., $\text{some}^{-1}(\{\bot\}) = \emptyset$.

WithBot.range_coe theorem

: range (some : α → WithBot α) = Ioi ⊥

Full source

theorem range_coe : range (some : α → WithBot α) = Ioi ⊥ :=
  @WithTop.range_coe αᵒᵈ _

Range of Canonical Embedding in $\text{WithBot} \alpha$ is $(\bot, \infty)$

Informal description

The range of the canonical embedding $\text{some} : \alpha \to \text{WithBot} \alpha$ is equal to the left-open right-infinite interval $(\bot, \infty)$ in $\text{WithBot} \alpha$, i.e., $\text{range}(\text{some}) = (\bot, \infty)$.

WithBot.preimage_coe_Ioi theorem

: (some : α → WithBot α) ⁻¹' Ioi a = Ioi a

Full source

@[simp]
theorem preimage_coe_Ioi : (some : α → WithBot α) ⁻¹' Ioi a = Ioi a :=
  ext fun _ => coe_lt_coe

Preimage of Ioi under WithBot embedding equals Ioi

Informal description

For any element $a$ in a preorder $\alpha$, the preimage of the left-open right-infinite interval $(a, \infty)$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot}\ \alpha$ is equal to the left-open right-infinite interval $(a, \infty)$ in $\alpha$.

WithBot.preimage_coe_Ici theorem

: (some : α → WithBot α) ⁻¹' Ici a = Ici a

Full source

@[simp]
theorem preimage_coe_Ici : (some : α → WithBot α) ⁻¹' Ici a = Ici a :=
  ext fun _ => coe_le_coe

Preimage of $[a, \infty)$ under WithBot embedding equals $[a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$, the preimage of the left-closed right-infinite interval $[a, \infty)$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot}\ \alpha$ is equal to the left-closed right-infinite interval $[a, \infty)$ in $\alpha$.

WithBot.preimage_coe_Iio theorem

: (some : α → WithBot α) ⁻¹' Iio a = Iio a

Full source

@[simp]
theorem preimage_coe_Iio : (some : α → WithBot α) ⁻¹' Iio a = Iio a :=
  ext fun _ => coe_lt_coe

Preimage of $(-\infty, a)$ under WithBot embedding equals $(-\infty, a)$

Informal description

For any element $a$ in a preorder $\alpha$, the preimage of the left-infinite right-open interval $(-\infty, a)$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot}\ \alpha$ is equal to the left-infinite right-open interval $(-\infty, a)$ in $\alpha$.

WithBot.preimage_coe_Iic theorem

: (some : α → WithBot α) ⁻¹' Iic a = Iic a

Full source

@[simp]
theorem preimage_coe_Iic : (some : α → WithBot α) ⁻¹' Iic a = Iic a :=
  ext fun _ => coe_le_coe

Preimage of $(-\infty, a]$ under $\text{some} : \alpha \to \text{WithBot} \alpha$ equals $(-\infty, a]$ in $\alpha$

Informal description

For any element $a$ in a preorder $\alpha$, the preimage of the left-infinite right-closed interval $(-\infty, a]$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot} \alpha$ is equal to the interval $(-\infty, a]$ in $\alpha$.

WithBot.preimage_coe_Icc theorem

: (some : α → WithBot α) ⁻¹' Icc a b = Icc a b

Full source

@[simp]
theorem preimage_coe_Icc : (some : α → WithBot α) ⁻¹' Icc a b = Icc a b := by simp [← Ici_inter_Iic]

Preimage of Closed Interval under WithBot Embedding Equals Original Interval

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the preimage of the closed interval $[a, b]$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot}\ \alpha$ is equal to the closed interval $[a, b]$ in $\alpha$.

WithBot.preimage_coe_Ico theorem

: (some : α → WithBot α) ⁻¹' Ico a b = Ico a b

Full source

@[simp]
theorem preimage_coe_Ico : (some : α → WithBot α) ⁻¹' Ico a b = Ico a b := by simp [← Ici_inter_Iio]

Preimage of $[a, b)$ under WithBot embedding equals $[a, b)$ in $\alpha$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the preimage of the left-closed right-open interval $[a, b)$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot}\ \alpha$ is equal to the interval $[a, b)$ in $\alpha$.

WithBot.preimage_coe_Ioc theorem

: (some : α → WithBot α) ⁻¹' Ioc a b = Ioc a b

Full source

@[simp]
theorem preimage_coe_Ioc : (some : α → WithBot α) ⁻¹' Ioc a b = Ioc a b := by simp [← Ioi_inter_Iic]

Preimage of $(a, b]$ under $\text{WithBot}$ embedding equals $(a, b]$ in $\alpha$

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the preimage of the left-open right-closed interval $(a, b]$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot}\ \alpha$ is equal to the interval $(a, b]$ in $\alpha$.

WithBot.preimage_coe_Ioo theorem

: (some : α → WithBot α) ⁻¹' Ioo a b = Ioo a b

Full source

@[simp]
theorem preimage_coe_Ioo : (some : α → WithBot α) ⁻¹' Ioo a b = Ioo a b := by simp [← Ioi_inter_Iio]

Preimage of Open Interval under WithBot Embedding Equals Open Interval

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the preimage of the open interval $(a, b)$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot}\ \alpha$ is equal to the open interval $(a, b)$ in $\alpha$.

WithBot.preimage_coe_Ioi_bot theorem

: (some : α → WithBot α) ⁻¹' Ioi ⊥ = univ

Full source

@[simp]
theorem preimage_coe_Ioi_bot : (some : α → WithBot α) ⁻¹' Ioi ⊥ = univ := by
  rw [← range_coe, preimage_range]

Preimage of $(\bot, \infty)$ under $\text{WithBot}$ embedding is universal set

Informal description

For any type $\alpha$ with a preorder, the preimage of the left-open right-infinite interval $(\bot, \infty)$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot}\ \alpha$ is equal to the entire set $\text{univ}$ (i.e., all elements of $\alpha$).

WithBot.preimage_coe_Ioc_bot theorem

: (some : α → WithBot α) ⁻¹' Ioc ⊥ a = Iic a

Full source

@[simp]
theorem preimage_coe_Ioc_bot : (some : α → WithBot α) ⁻¹' Ioc ⊥ a = Iic a := by
  simp [← Ioi_inter_Iic]

Preimage of $(\bot, a]$ under $\text{WithBot}$ embedding equals $(-\infty, a]$ in $\alpha$

Informal description

For any element $a$ in a preorder $\alpha$, the preimage of the left-open right-closed interval $(\bot, a]$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot}\ \alpha$ is equal to the left-infinite right-closed interval $(-\infty, a]$ in $\alpha$.

WithBot.preimage_coe_Ioo_bot theorem

: (some : α → WithBot α) ⁻¹' Ioo ⊥ a = Iio a

Full source

@[simp]
theorem preimage_coe_Ioo_bot : (some : α → WithBot α) ⁻¹' Ioo ⊥ a = Iio a := by
  simp [← Ioi_inter_Iio]

Preimage of $(\bot, a)$ under WithBot embedding equals $(-\infty, a)$

Informal description

For any element $a$ in a preorder $\alpha$, the preimage of the open interval $(\bot, a)$ in $\text{WithBot}\ \alpha$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot}\ \alpha$ is equal to the left-infinite right-open interval $(-\infty, a)$ in $\alpha$.

WithBot.image_coe_Iio theorem

: (some : α → WithBot α) '' Iio a = Ioo (⊥ : WithBot α) a

Full source

theorem image_coe_Iio : (some : α → WithBot α) '' Iio a = Ioo (⊥ : WithBot α) a := by
  rw [← preimage_coe_Iio, image_preimage_eq_inter_range, range_coe, inter_comm, Ioi_inter_Iio]

Image of $(-\infty, a)$ under WithBot embedding equals $(\bot, a)$ in WithBot

Informal description

For any element $a$ in a preorder $\alpha$, the image of the left-infinite right-open interval $(-\infty, a)$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot}\ \alpha$ is equal to the open interval $(\bot, a)$ in $\text{WithBot}\ \alpha$.

WithBot.image_coe_Iic theorem

: (some : α → WithBot α) '' Iic a = Ioc (⊥ : WithBot α) a

Full source

theorem image_coe_Iic : (some : α → WithBot α) '' Iic a = Ioc (⊥ : WithBot α) a := by
  rw [← preimage_coe_Iic, image_preimage_eq_inter_range, range_coe, inter_comm, Ioi_inter_Iic]

Image of $(-\infty, a]$ under WithBot embedding equals $(\bot, a]$ in WithBot

Informal description

For any element $a$ in a preorder $\alpha$, the image of the left-infinite right-closed interval $(-\infty, a]$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot}\ \alpha$ is equal to the left-open right-closed interval $(\bot, a]$ in $\text{WithBot}\ \alpha$.

WithBot.image_coe_Ioi theorem

: (some : α → WithBot α) '' Ioi a = Ioi (a : WithBot α)

Full source

theorem image_coe_Ioi : (some : α → WithBot α) '' Ioi a = Ioi (a : WithBot α) := by
  rw [← preimage_coe_Ioi, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Ioi_subset_Ioi bot_le)]

Image of $(a, \infty)$ under WithBot embedding equals $(a, \infty)$ in WithBot

Informal description

For any element $a$ in a preorder $\alpha$, the image of the left-open right-infinite interval $(a, \infty)$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot}\ \alpha$ is equal to the left-open right-infinite interval $(a, \infty)$ in $\text{WithBot}\ \alpha$.

WithBot.image_coe_Ici theorem

: (some : α → WithBot α) '' Ici a = Ici (a : WithBot α)

Full source

theorem image_coe_Ici : (some : α → WithBot α) '' Ici a = Ici (a : WithBot α) := by
  rw [← preimage_coe_Ici, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Ici_subset_Ioi.2 <| bot_lt_coe a)]

Image of $[a, \infty)$ under WithBot embedding equals $[a, \infty)$ in WithBot

Informal description

For any element $a$ in a preorder $\alpha$, the image of the left-closed right-infinite interval $[a, \infty)$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot}\ \alpha$ is equal to the left-closed right-infinite interval $[a, \infty)$ in $\text{WithBot}\ \alpha$.

WithBot.image_coe_Icc theorem

: (some : α → WithBot α) '' Icc a b = Icc (a : WithBot α) b

Full source

theorem image_coe_Icc : (some : α → WithBot α) '' Icc a b = Icc (a : WithBot α) b := by
  rw [← preimage_coe_Icc, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left
      (Subset.trans Icc_subset_Ici_self <| Ici_subset_Ioi.2 <| bot_lt_coe a)]

Image of Closed Interval under WithBot Embedding Equals Closed Interval in WithBot

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the image of the closed interval $[a, b]$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot}\ \alpha$ is equal to the closed interval $[a, b]$ in $\text{WithBot}\ \alpha$.

WithBot.image_coe_Ioc theorem

: (some : α → WithBot α) '' Ioc a b = Ioc (a : WithBot α) b

Full source

theorem image_coe_Ioc : (some : α → WithBot α) '' Ioc a b = Ioc (a : WithBot α) b := by
  rw [← preimage_coe_Ioc, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Subset.trans Ioc_subset_Ioi_self <| Ioi_subset_Ioi bot_le)]

Image of $(a, b]$ under WithBot embedding equals $(a, b]$ in WithBot

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the image of the left-open right-closed interval $(a, b]$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot}\ \alpha$ is equal to the left-open right-closed interval $(a, b]$ in $\text{WithBot}\ \alpha$.

WithBot.image_coe_Ico theorem

: (some : α → WithBot α) '' Ico a b = Ico (a : WithBot α) b

Full source

theorem image_coe_Ico : (some : α → WithBot α) '' Ico a b = Ico (a : WithBot α) b := by
  rw [← preimage_coe_Ico, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left
      (Subset.trans Ico_subset_Ici_self <| Ici_subset_Ioi.2 <| bot_lt_coe a)]

Image of $[a, b)$ under WithBot embedding equals $[a, b)$ in WithBot

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the image of the left-closed right-open interval $[a, b)$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot}\ \alpha$ is equal to the left-closed right-open interval $[a, b)$ in $\text{WithBot}\ \alpha$.

WithBot.image_coe_Ioo theorem

: (some : α → WithBot α) '' Ioo a b = Ioo (a : WithBot α) b

Full source

theorem image_coe_Ioo : (some : α → WithBot α) '' Ioo a b = Ioo (a : WithBot α) b := by
  rw [← preimage_coe_Ioo, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Subset.trans Ioo_subset_Ioi_self <| Ioi_subset_Ioi bot_le)]

Image of Open Interval under WithBot Embedding Equals Open Interval in WithBot

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the image of the open interval $(a, b)$ under the canonical embedding $\text{some} : \alpha \to \text{WithBot}\ \alpha$ is equal to the open interval $(a, b)$ in $\text{WithBot}\ \alpha$.