continuousMapEquivOfConnectedSpace

English

There is a bijection between C(X,Y) and Y when Y is totally disconnected and X is connected.

Русский

Существует биекция между множеством непрерывных отображений C(X,Y) и Y, если Y полностью раздельно и X неразрывно.

LaTeX

$$C(X,Y) \cong Y$$

Lean4

/-- The bijection `C(X, Y) ≃ Y` when `Y` is totally disconnected and `X` is connected. -/
@[simps! symm_apply_apply]
noncomputable def continuousMapEquivOfConnectedSpace (X Y : Type*) [TopologicalSpace X] [TopologicalSpace Y]
    [TotallyDisconnectedSpace Y] [ConnectedSpace X] : C(X, Y) ≃ Y
    where
  toFun f := f (Classical.arbitrary _)
  invFun y := ⟨fun _ ↦ y, by continuity⟩
  left_inv f := ContinuousMap.ext (TotallyDisconnectedSpace.eq_of_continuous _ f.2 _)
  right_inv _ := rfl

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