toContinuousMap — Mathlib

English

The conversion from a ContinuousOrderHom to a ContinuousMap preserves continuity.

Русский

Преобразование непрерывного монотонного отображения в непрерывное отображение сохраняет непрерывность.

LaTeX

$$ContinuousOrderHom.toContinuousMap (f) : C(α,β)$$

Lean4

/-- Reinterpret a `ContinuousOrderHom` as a `ContinuousMap`. -/
def toContinuousMap (f : α →Co β) : C(α, β) :=
  { f with }

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