toTopHomClass — Mathlib

English

Esakia morphisms give rise to a TopHomClass structure; i.e., morphisms compatible with the topological and order structures can be organized into a TopHomClass.

Русский

Эзакья-морфизмы образуют структуру TopHomClass; то есть морфизмы, совместимые с топологической и порядковой структурами, образуют класс TopHomClass.

LaTeX

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

Lean4

instance (priority := 100) toTopHomClass [PartialOrder α] [OrderTop α] [Preorder β] [OrderTop β]
    [PseudoEpimorphismClass F α β] : TopHomClass F α β where
  map_top
    f := by
    let ⟨b, h⟩ := exists_map_eq_of_map_le f (@le_top _ _ _ <| f ⊤)
    rw [← top_le_iff.1 h.1, h.2]
      -- See note [lower instance priority]

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