tendsto_comap'_iff — Mathlib

English

If range i ∈ f, then Tendsto (m ∘ i) (comap i f) g ↔ Tendsto m f g.

Русский

Если range i ∈ f, тогда Tendsto (m ∘ i) (comap i f) g ↔ Tendsto m f g.

LaTeX

$$$\\forall m:\\alpha \\to \\beta, \\forall f:\\mathrm{Filter}(\\alpha), \\forall g:\\mathrm{Filter}(\\beta), \\forall i:\\gamma \\to \\alpha, (\\mathrm{range}\; i \\in f) \\Rightarrow \\mathrm{Tendsto} (m \\circ i) (\\mathrm{comap} i f) g \\iff \\mathrm{Tendsto} m f g$$$

Lean4

theorem tendsto_comap'_iff {m : α → β} {f : Filter α} {g : Filter β} {i : γ → α} (h : range i ∈ f) :
    Tendsto (m ∘ i) (comap i f) g ↔ Tendsto m f g :=
  by
  rw [Tendsto, ← map_compose]
  simp only [(· ∘ ·), map_comap_of_mem h, Tendsto]

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