continuous_comp_iff — Mathlib

English

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

Русский

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

LaTeX

$$$\mathrm{ContinuousAt}(g \circ f, x) \iff \mathrm{ContinuousAt}(g, f(x))$ under IsOpenQuotientMap f$$

Lean4

theorem continuous_comp_iff (h : IsOpenQuotientMap f) {g : Y → Z} : Continuous (g ∘ f) ↔ Continuous g :=
  h.isQuotientMap.continuous_iff.symm

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