liminf_add_of_left_tendsto_zero — Mathlib

English

If a function f tends to 0 along a filter u, then liminf_u (f + g) = liminf_u g for any g: ι → ENNReal.

Русский

Если функция f стремится к нулю по фильтру u, то liminf_u (f + g) = liminf_u g для любой g.

LaTeX

$$$$\\text{If } u \\xrightarrow{T} 0\\text{, then } \\liminf_{u} (f + g) = \\liminf_{u} g.$$$$

Lean4

theorem liminf_add_of_left_tendsto_zero {u : Filter ι} {f : ι → ℝ≥0∞} (hf : u.Tendsto f (𝓝 0)) (g : ι → ℝ≥0∞) :
    u.liminf (f + g) = u.liminf g := by rw [add_comm, liminf_add_of_right_tendsto_zero hf]

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