Mathlib.Order.Filter.AtTopBot.Map

OrderIso.comap_atTop theorem

(e : α ≃o β) : comap e atTop = atTop

Full source

@[simp]
theorem comap_atTop (e : α ≃o β) : comap e atTop = atTop := by
  simp [atTop, ← e.surjective.iInf_comp]

Preimage of `atTop` Filter under Order Isomorphism Equals `atTop` Filter

Informal description

Let $\alpha$ and $\beta$ be preordered types and let $e : \alpha \simeq_o \beta$ be an order isomorphism between them. Then the preimage filter of the `atTop` filter on $\beta$ under $e$ is equal to the `atTop` filter on $\alpha$, i.e., $$ e^{-1}(\text{atTop}_\beta) = \text{atTop}_\alpha. $$

OrderIso.comap_atBot theorem

(e : α ≃o β) : comap e atBot = atBot

Full source

@[simp]
theorem comap_atBot (e : α ≃o β) : comap e atBot = atBot :=
  e.dual.comap_atTop

Preimage of `atBot` Filter under Order Isomorphism Equals `atBot` Filter

Informal description

Let $\alpha$ and $\beta$ be preordered types and let $e : \alpha \simeq_o \beta$ be an order isomorphism between them. Then the preimage filter of the `atBot` filter on $\beta$ under $e$ is equal to the `atBot` filter on $\alpha$, i.e., $$ e^{-1}(\text{atBot}_\beta) = \text{atBot}_\alpha. $$

OrderIso.map_atTop theorem

(e : α ≃o β) : map (e : α → β) atTop = atTop

Full source

@[simp]
theorem map_atTop (e : α ≃o β) : map (e : α → β) atTop = atTop := by
  rw [← e.comap_atTop, map_comap_of_surjective e.surjective]

Image of `atTop` Filter under Order Isomorphism Equals `atTop` Filter

Informal description

Let $\alpha$ and $\beta$ be preordered types and let $e : \alpha \simeq_o \beta$ be an order isomorphism between them. Then the image of the `atTop` filter on $\alpha$ under $e$ is equal to the `atTop` filter on $\beta$, i.e., $$ e(\text{atTop}_\alpha) = \text{atTop}_\beta. $$

OrderIso.map_atBot theorem

(e : α ≃o β) : map (e : α → β) atBot = atBot

Full source

@[simp]
theorem map_atBot (e : α ≃o β) : map (e : α → β) atBot = atBot :=
  e.dual.map_atTop

Image of `atBot` Filter under Order Isomorphism Equals `atBot` Filter

Informal description

Let $\alpha$ and $\beta$ be preordered types and let $e : \alpha \simeq_o \beta$ be an order isomorphism between them. Then the image of the `atBot` filter on $\alpha$ under $e$ is equal to the `atBot` filter on $\beta$, i.e., $$ e(\text{atBot}_\alpha) = \text{atBot}_\beta. $$

OrderIso.tendsto_atTop theorem

(e : α ≃o β) : Tendsto e atTop atTop

Full source

theorem tendsto_atTop (e : α ≃o β) : Tendsto e atTop atTop :=
  e.map_atTop.le

Order Isomorphism Preserves Limit to Positive Infinity ($\lim e = \text{atTop}_\beta$ at $\text{atTop}_\alpha$)

Informal description

Let $\alpha$ and $\beta$ be preordered types and let $e : \alpha \simeq_o \beta$ be an order isomorphism between them. Then the function $e$ tends to the filter at positive infinity on $\beta$ as its input tends to the filter at positive infinity on $\alpha$, i.e., $$ \lim_{x \to \text{atTop}_\alpha} e(x) = \text{atTop}_\beta. $$

OrderIso.tendsto_atBot theorem

(e : α ≃o β) : Tendsto e atBot atBot

Full source

theorem tendsto_atBot (e : α ≃o β) : Tendsto e atBot atBot :=
  e.map_atBot.le

Order Isomorphism Preserves Limit to Negative Infinity ($\lim e = \text{atBot}_\beta$ at $\text{atBot}_\alpha$)

Informal description

Let $\alpha$ and $\beta$ be preordered types and let $e : \alpha \simeq_o \beta$ be an order isomorphism between them. Then the function $e$ tends to the filter at negative infinity on $\beta$ as its input tends to the filter at negative infinity on $\alpha$, i.e., $$ \lim_{x \to \text{atBot}_\alpha} e(x) = \text{atBot}_\beta. $$

OrderIso.tendsto_atTop_iff theorem

{l : Filter γ} {f : γ → α} (e : α ≃o β) : Tendsto (fun x => e (f x)) l atTop ↔ Tendsto f l atTop

Full source

@[simp]
theorem tendsto_atTop_iff {l : Filter γ} {f : γ → α} (e : α ≃o β) :
    TendstoTendsto (fun x => e (f x)) l atTop ↔ Tendsto f l atTop := by
  rw [← e.comap_atTop, tendsto_comap_iff, Function.comp_def]

Order Isomorphism Preserves Tendency to Positive Infinity ($\lim e \circ f = \text{atTop}_\beta \Leftrightarrow \lim f = \text{atTop}_\alpha$)

Informal description

Let $\alpha$ and $\beta$ be preordered types, $e : \alpha \simeq_o \beta$ an order isomorphism, $γ$ a type with a filter $l$, and $f : γ \to \alpha$ a function. Then the composition $e \circ f$ tends to $\text{atTop}_\beta$ along $l$ if and only if $f$ tends to $\text{atTop}_\alpha$ along $l$. In other words: $$ \lim_{x \to l} e(f(x)) = \text{atTop}_\beta \quad \Leftrightarrow \quad \lim_{x \to l} f(x) = \text{atTop}_\alpha. $$

OrderIso.tendsto_atBot_iff theorem

{l : Filter γ} {f : γ → α} (e : α ≃o β) : Tendsto (fun x => e (f x)) l atBot ↔ Tendsto f l atBot

Full source

@[simp]
theorem tendsto_atBot_iff {l : Filter γ} {f : γ → α} (e : α ≃o β) :
    TendstoTendsto (fun x => e (f x)) l atBot ↔ Tendsto f l atBot :=
  e.dual.tendsto_atTop_iff

Order Isomorphism Preserves Tendency to Negative Infinity ($\lim e \circ f = \text{atBot}_\beta \Leftrightarrow \lim f = \text{atBot}_\alpha$)

Informal description

Let $\alpha$ and $\beta$ be preordered types, $e : \alpha \simeq_o \beta$ an order isomorphism, $γ$ a type with a filter $l$, and $f : γ \to \alpha$ a function. Then the composition $e \circ f$ tends to $\text{atBot}_\beta$ along $l$ if and only if $f$ tends to $\text{atBot}_\alpha$ along $l$. In other words: $$ \lim_{x \to l} e(f(x)) = \text{atBot}_\beta \quad \Leftrightarrow \quad \lim_{x \to l} f(x) = \text{atBot}_\alpha. $$