connectedComponentsLift_continuous

English

If f: α → β is continuous, then the induced lift to connected components, h.connectedComponentsLift, is also continuous.

Русский

Если отображение f: α → β непрерывно, то соответствующий лифт на множество компонент связности, h.connectedComponentsLift, тоже непрерывен.

LaTeX

$$$\text{Continuous}(h.\text{connectedComponentsLift})$$$

Lean4

@[continuity]
theorem connectedComponentsLift_continuous (h : Continuous f) : Continuous h.connectedComponentsLift :=
  h.quotient_liftOn' <| by convert h.image_eq_of_connectedComponent_eq

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