Mathlib.Order.Interval.Set.OrderEmbedding

OrderEmbedding.preimage_Ici theorem

: e ⁻¹' Ici (e x) = Ici x

Full source

@[simp] theorem preimage_Ici : e ⁻¹' Ici (e x) = Ici x := ext fun _ ↦ e.le_iff_le

Preimage of Closed Right-Infinite Interval under Order Embedding

Informal description

For an order embedding $e : \alpha \hookrightarrow \beta$ and any element $x \in \alpha$, the preimage under $e$ of the closed right-infinite interval $[e(x), \infty)$ in $\beta$ is equal to the closed right-infinite interval $[x, \infty)$ in $\alpha$, i.e., $$ e^{-1}\big([e(x), \infty)\big) = [x, \infty). $$

OrderEmbedding.preimage_Iic theorem

: e ⁻¹' Iic (e x) = Iic x

Full source

@[simp] theorem preimage_Iic : e ⁻¹' Iic (e x) = Iic x := ext fun _ ↦ e.le_iff_le

Preimage of Closed Left-Infinite Interval under Order Embedding

Informal description

For an order embedding $e : \alpha \hookrightarrow \beta$ and any element $x \in \alpha$, the preimage under $e$ of the closed left-infinite interval $(-\infty, e(x)]$ in $\beta$ is equal to the closed left-infinite interval $(-\infty, x]$ in $\alpha$, i.e., $$ e^{-1}\big((-\infty, e(x)]\big) = (-\infty, x]. $$

OrderEmbedding.preimage_Ioi theorem

: e ⁻¹' Ioi (e x) = Ioi x

Full source

@[simp] theorem preimage_Ioi : e ⁻¹' Ioi (e x) = Ioi x := ext fun _ ↦ e.lt_iff_lt

Preimage of Strict Right-Infinite Interval under Order Embedding

Informal description

For an order embedding $e : \alpha \hookrightarrow \beta$ and any element $x \in \alpha$, the preimage under $e$ of the strict right-infinite interval $(e(x), \infty)$ in $\beta$ is equal to the strict right-infinite interval $(x, \infty)$ in $\alpha$, i.e., $$ e^{-1}\big((e(x), \infty)\big) = (x, \infty). $$

OrderEmbedding.preimage_Iio theorem

: e ⁻¹' Iio (e x) = Iio x

Full source

@[simp] theorem preimage_Iio : e ⁻¹' Iio (e x) = Iio x := ext fun _ ↦ e.lt_iff_lt

Preimage of Strict Left-Infinite Interval under Order Embedding

Informal description

For an order embedding $e$ and any element $x$ in its domain, the preimage under $e$ of the strict left-infinite interval $(-\infty, e(x))$ in the codomain is equal to the strict left-infinite interval $(-\infty, x)$ in the domain, i.e., $e^{-1}((-\infty, e(x))) = (-\infty, x)$.

OrderEmbedding.preimage_Icc theorem

: e ⁻¹' Icc (e x) (e y) = Icc x y

Full source

@[simp] theorem preimage_Icc : e ⁻¹' Icc (e x) (e y) = Icc x y := by ext; simp

Preimage of Closed Interval under Order Embedding

Informal description

Let $e : \alpha \hookrightarrow \beta$ be an order embedding between partially ordered sets $\alpha$ and $\beta$. For any elements $x, y \in \alpha$, the preimage under $e$ of the closed interval $[e(x), e(y)]$ in $\beta$ is equal to the closed interval $[x, y]$ in $\alpha$. That is, $$ e^{-1}\big([e(x), e(y)]\big) = [x, y]. $$

OrderEmbedding.preimage_Ico theorem

: e ⁻¹' Ico (e x) (e y) = Ico x y

Full source

@[simp] theorem preimage_Ico : e ⁻¹' Ico (e x) (e y) = Ico x y := by ext; simp

Preimage of Closed-Open Interval under Order Embedding

Informal description

Let $e : \alpha \hookrightarrow \beta$ be an order embedding between partially ordered sets $\alpha$ and $\beta$. For any elements $x, y \in \alpha$, the preimage under $e$ of the closed-open interval $[e(x), e(y))$ in $\beta$ is equal to the closed-open interval $[x, y)$ in $\alpha$. That is, $$ e^{-1}\big([e(x), e(y))\big) = [x, y). $$

OrderEmbedding.preimage_Ioc theorem

: e ⁻¹' Ioc (e x) (e y) = Ioc x y

Full source

@[simp] theorem preimage_Ioc : e ⁻¹' Ioc (e x) (e y) = Ioc x y := by ext; simp

Preimage of Open-Closed Interval under Order Embedding

Informal description

Let $e : \alpha \hookrightarrow \beta$ be an order embedding between partially ordered sets $\alpha$ and $\beta$. For any elements $x, y \in \alpha$, the preimage under $e$ of the open-closed interval $(e(x), e(y)]$ in $\beta$ is equal to the open-closed interval $(x, y]$ in $\alpha$. That is, $$ e^{-1}\big((e(x), e(y)]\big) = (x, y]. $$

OrderEmbedding.preimage_Ioo theorem

: e ⁻¹' Ioo (e x) (e y) = Ioo x y

Full source

@[simp] theorem preimage_Ioo : e ⁻¹' Ioo (e x) (e y) = Ioo x y := by ext; simp

Preimage of Open Interval under Order Embedding

Informal description

Let $e : \alpha \hookrightarrow \beta$ be an order embedding between partially ordered sets $\alpha$ and $\beta$. For any elements $x, y \in \alpha$, the preimage under $e$ of the open interval $(e(x), e(y))$ in $\beta$ is equal to the open interval $(x, y)$ in $\alpha$. That is, $$ e^{-1}\big((e(x), e(y))\big) = (x, y). $$

OrderEmbedding.preimage_uIcc theorem

[Lattice β] (e : α ↪o β) (x y : α) : e ⁻¹' (uIcc (e x) (e y)) = uIcc x y

Full source

@[simp] theorem preimage_uIcc [Lattice β] (e : α ↪o β) (x y : α) :
    e ⁻¹' (uIcc (e x) (e y)) = uIcc x y := by
  cases le_total x y <;> simp [*]

Preimage of Lattice Interval under Order Embedding

Informal description

Let $\alpha$ be a partially ordered set and $\beta$ be a lattice. Given an order embedding $e : \alpha \hookrightarrow \beta$ and elements $x, y \in \alpha$, the preimage under $e$ of the interval $[e(x) \sqcap e(y), e(x) \sqcup e(y)]$ in $\beta$ is equal to the interval $[x \sqcap y, x \sqcup y]$ in $\alpha$. That is, $$ e^{-1}\big([e(x) \sqcap e(y), e(x) \sqcup e(y)]\big) = [x \sqcap y, x \sqcup y]. $$

OrderEmbedding.preimage_uIoc theorem

[LinearOrder β] (e : α ↪o β) (x y : α) : e ⁻¹' (uIoc (e x) (e y)) = uIoc x y

Full source

@[simp] theorem preimage_uIoc [LinearOrder β] (e : α ↪o β) (x y : α) :
    e ⁻¹' (uIoc (e x) (e y)) = uIoc x y := by
  cases le_total x y <;> simp [*]

Preimage of Generalized Open-Closed Interval under Order Embedding

Informal description

Let $\alpha$ be a partially ordered set and $\beta$ be a linearly ordered set. Given an order embedding $e : \alpha \hookrightarrow \beta$ and elements $x, y \in \alpha$, the preimage under $e$ of the interval $(e(x) \sqcap e(y), e(x) \sqcup e(y)]$ in $\beta$ is equal to the interval $(x \sqcap y, x \sqcup y]$ in $\alpha$. That is, $$ e^{-1}\big((\min(e(x), e(y)), \max(e(x), e(y))]\big) = (\min(x, y), \max(x, y)]. $$