tendsto_comap_iff — Mathlib

English

For f: α → β, l1 on α, l2 on γ, Tendsto f l1 (comap g l2) is equivalent to Tendsto (g ∘ f) l1 l2.

Русский

Для f: α → β, l1 на α, l2 на γ, Tendsto f l1 (comap g l2 эквивалентно Tendsto (g ∘ f) l1 l2).

LaTeX

$$$\\forall f:\\alpha \\to \\beta, \\forall l_1:\\mathrm{Filter}(\\alpha), \\forall l_2:\\mathrm{Filter}(\\gamma),\\; \\mathrm{Tendsto} f l_1 (\\mathrm{comap} g l_2) \\iff \\mathrm{Tendsto} (g \\circ f) l_1 l_2$$$

Lean4

@[simp]
theorem tendsto_comap_iff {f : α → β} {g : β → γ} {a : Filter α} {c : Filter γ} :
    Tendsto f a (c.comap g) ↔ Tendsto (g ∘ f) a c :=
  ⟨fun h => tendsto_comap.comp h, fun h => map_le_iff_le_comap.mp <| by rwa [map_map]⟩

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