tendsto_sub_const_iff — Mathlib

English

In an additive topological group, for any b, Tendsto (f(k) − b) to (c − b) iff Tendsto f(k) to c.

Русский

В аддитивной топологической группе для любого b: Tendsto (f(k) − b) к (c − b) эквивалентно Tendsto f(k) к c.

LaTeX

$$$\text{Tendsto}(f)_{l}(\mathcal{N}(c)) \iff \text{Tendsto}(f(k) - b)_{l}(\mathcal{N}(c - b)).$$$

Lean4

theorem tendsto_sub_const_iff {G : Type*} [AddCommGroup G] [TopologicalSpace G] [ContinuousSub G] (b : G) {c : G}
    {f : α → G} {l : Filter α} : Tendsto (f · - b) l (𝓝 (c - b)) ↔ Tendsto f l (𝓝 c) :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ Filter.Tendsto.sub_const h b⟩
  convert h.sub_const (-b) with k <;> rw [sub_sub, ← sub_eq_add_neg, sub_self, sub_zero]

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