continuous_quot_mk — Mathlib

English

Let X be a topological space and ~ an equivalence relation on X. The canonical quotient map q: X → X/∼ is continuous.

Русский

Пусть X — топологическое пространство и ∼ — эквивалентность на X. Каноническая факторная карта q: X → X/∼ непрерывна.

LaTeX

$$$$ \mathrm{Continuous}(\pi) $$$$

Lean4

@[continuity, fun_prop]
theorem continuous_quot_mk : Continuous (@Quot.mk X r) :=
  continuous_coinduced_rng

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