instContinuousOrderHomClass — Mathlib

English

The class of continuous order-preserving maps from α to β, denoted α →Co β, consists of those maps that are monotone and continuous. In particular, the class is defined by requiring monotonicity and continuity for each map.

Русский

Класс отображений α →Co β состоит из отображений, сохраняющих порядок и непрерывных. Каждое отображение в этом классе является монотонным и непрерывным.

LaTeX

$$$\text{ContinuousOrderHomClass}(F,\alpha,\beta) \iff \forall f \in F,\; \text{monotone}(f) \wedge \text{continuous}(f).$$$

Lean4

instance : ContinuousOrderHomClass (α →Co β) α β
    where
  map_monotone f := f.monotone'
  map_continuous f := f.continuous_toFun

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