tendsto_const — Mathlib

English

If u is asymptotically equivalent to a constant function, then u tends to that constant.

Русский

Если u асимптотически эквивалентна константе, то u стремится к этой константе.

LaTeX

$$$u ~[l] const_ c \Rightarrow Tendsto u l (nhds c)$$$

Lean4

theorem tendsto_const {c : β} (hu : u ~[l] const _ c) : Tendsto u l (𝓝 c) :=
  by
  rcases em <| c = 0 with rfl | h
  · exact (tendsto_congr' <| isEquivalent_zero_iff_eventually_zero.mp hu).mpr tendsto_const_nhds
  · exact (isEquivalent_const_iff_tendsto h).mp hu

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