instOrderHomClassContinuousHom — Mathlib

English

Continuous maps α →𝒄 β form an OrderHomClass from α to β, i.e., they respect the order relation via monotonicity.

Русский

Непрерывные отображения α →𝒄 β образуют класс ордер-гомоморфизмов между α и β, то есть сохраняют порядок.

LaTeX

$$$\text{OrderHomClass} (α \to𝒄 β) α β$$$

Lean4

instance : OrderHomClass (α →𝒄 β) α β where map_rel f _ _ h := f.mono h

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