instPathConnectedSpace — Mathlib

English

If X is path-connected and s is a setoid on X, then the quotient (Quotient s) is path-connected.

Русский

Если X путево связано и задана эквивалентность, то фактор-пространство по отношению к ней путево связано.

LaTeX

$$PathConnectedSpace (Quotient s)$$

Lean4

instance instPathConnectedSpace {s : Setoid X} [PathConnectedSpace X] : PathConnectedSpace (Quotient s) :=
  Quotient.mk'_surjective.pathConnectedSpace continuous_coinduced_rng

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