tendsto_atBot' — Mathlib

English

Dual to tendsto_atTop', Tendsto f atBot l is equivalent to: for every s in l there exists a such that for all b with b ≥ a, f(b) ∈ s.

Русский

Дуал к tendsto_atTop': Tendsto f atBot l эквивалентно: для каждого множества s из l существует a, такое что для всех b ≥ a, f(b) ∈ s.

LaTeX

$$$\forall\!{f},\ Tendsto f\ atBot\ l \leftrightarrow \forall s\in l, \exists a, \forall b \ge a, f(b) \in s$$$

Lean4

theorem tendsto_atBot' : Tendsto f atBot l ↔ ∀ s ∈ l, ∃ a, ∀ b ≤ a, f b ∈ s :=
  tendsto_atTop' (α := αᵒᵈ)

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