instCoeTCEsakiaHomOfEsakiaHomClass

English

There is a coercion from any function-like family F that is Esakia-homomorphic to EsakiaHom α β, realized as a CoeTC instance.

Русский

Существует приведение типа от любой функции, являющейся Esakia-гомоморфизмом, к EsakiaHom α β, реализуемое как инстанс CoeTC.

LaTeX

$$$\text{instCoeTC } F (EsakiaHom \alpha \beta)$$$

Lean4

instance [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [EsakiaHomClass F α β] :
    CoeTC F (EsakiaHom α β) :=
  ⟨fun f => ⟨f, exists_map_eq_of_map_le f⟩⟩

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