instConnectedSpace — Mathlib

English

If α is connected and s is a setoid on α, then the quotient space α modulo s is connected.

Русский

Если α связано, то фактор-пространство α/≈ по произвольному эквивалентному отношению связано.

LaTeX

$$$$ConnectedSpace(\\mathrm{Quotient}(s))$$$$

Lean4

instance instConnectedSpace {s : Setoid α} [ConnectedSpace α] : ConnectedSpace (Quotient s) :=
  Quotient.mk'_surjective.connectedSpace continuous_coinduced_rng

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