English
If a is finite and f(n) ≤ a for all n, then Tendsto(a−f(n)) to 0 is equivalent to Tendsto(f(n)) to a.
Русский
Если a конечна и f(n)≤a для всех n, то сходство (a−f(n))→0 эквивалентно f(n)→a.
LaTeX
$$$a\\neq \\infty$, (∀n, f(n) \\le a) \\implies\\left(\\mathrm{Tendsto}(n \\mapsto a-f(n))\\ f\\to 0 \\right) \\\\iff \\left(\\mathrm{Tendsto}(n \\mapsto f(n))\\ f\\to a \\right)$$
Lean4
theorem tendsto_const_sub_nhds_zero_iff {l : Filter α} {f : α → ℝ≥0∞} {a : ℝ≥0∞} (ha : a ≠ ∞) (hfa : ∀ n, f n ≤ a) :
Tendsto (fun n ↦ a - f n) l (𝓝 0) ↔ Tendsto (fun n ↦ f n) l (𝓝 a) :=
by
rw [ENNReal.tendsto_nhds_zero, ENNReal.tendsto_nhds ha]
refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ?_⟩
· filter_upwards [h ε hε] with n hn
refine ⟨?_, (hfa n).trans (le_add_right le_rfl)⟩
rw [tsub_le_iff_right] at hn ⊢
rwa [add_comm]
· filter_upwards [h ε hε] with n hn
have hN_left := hn.1
rw [tsub_le_iff_right] at hN_left ⊢
rwa [add_comm]
