tendsto_nhds_iff — Mathlib

English

For any c, the tendsto of u to nhds c is equivalent to the tendsto of v to nhds c when u ~[l] v.

Русский

Для любого c стремление u к nhds c эквивалентно стремлению v к nhds c при условии u ~[l] v.

LaTeX

$$huv : u ~[l] v ⟹ (Tendsto u l (nhds c) ↔ Tendsto v l (nhds c))$$

Lean4

theorem tendsto_nhds_iff {c : β} (huv : u ~[l] v) : Tendsto u l (𝓝 c) ↔ Tendsto v l (𝓝 c) :=
  ⟨huv.tendsto_nhds, huv.symm.tendsto_nhds⟩

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