tendsto_comp_val_Iio_atBot — Mathlib

English

For a preorder α with appropriate directedness and NoMinOrder, Tendsto on Iio a to l atBot is equivalent to Tendsto on α to l atBot.

Русский

Для порядковой системы α с направленностью и отсутствием минимального элемента, схождение на подмножество Iio a эквивалентно обычной схождению к нижней граннице.

LaTeX

$$$\text{Tendsto} (f \circ \iota) \, l \, \text{atBot} \\iff \\ \text{Tendsto} f \, l \, \text{atBot}$$$

Lean4

@[simp]
theorem tendsto_comp_val_Iio_atBot [Preorder α] [IsDirected α (· ≥ ·)] [NoMinOrder α] {a : α} {f : α → β}
    {l : Filter β} : Tendsto (fun x : Iio a => f x) atBot l ↔ Tendsto f atBot l :=
  tendsto_comp_val_Ioi_atTop (α := αᵒᵈ)

Похожие утверждения