continuousAt_comp_iff — Mathlib

English

For IsOpenQuotientMap f, continuousAt of g ∘ f at x is equivalent to continuousAt of g at f x.

Русский

Для IsOpenQuotientMap f непрерывность g ∘ f в x эквивалентна непрерывности g в f(x).

LaTeX

$$$\mathrm{continuousAt}\,(g \circ f)\ x \iff \mathrm{continuousAt}\,g\,(f x)$$$

Lean4

theorem continuousAt_comp_iff (h : IsOpenQuotientMap f) {g : Y → Z} {x : X} :
    ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x) := by
  simp only [ContinuousAt, ← h.map_nhds_eq, tendsto_map'_iff, comp_def]

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