toPseudoEpimorphismClass — Mathlib

English

From Esakia morphisms one obtains a PseudoEpimorphismClass; i.e., the class of Esakia morphisms is compatible with the pseudo-epimorphism structure.

Русский

Из Esakia-гомоморфизмов образуется класс PseudoEpimorphismClass; то есть класс Esakia-гомоморфизмов совместим с структурой псевдоэпиморфизмов.

LaTeX

$$$\text{EsakiaHomClass } F \alpha \beta \Rightarrow \text{PseudoEpimorphismClass } F \alpha \beta$$$

Lean4

instance (priority := 100) toPseudoEpimorphismClass [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β]
    [EsakiaHomClass F α β] : PseudoEpimorphismClass F α β :=
  { ‹EsakiaHomClass F α β› with map_rel := ContinuousOrderHomClass.map_monotone }

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