toContinuousOrderHom_coe — Mathlib

English

For any Esakia morphism f, its associated continuous-order morphism has the same underlying function as f itself; i.e., the mapping of f as an Esakia morphism coincides with the underlying function of its continuous-order representation.

Русский

Для любого морфизма Эзякия выполняется, что отображение f как непрерывного порядкового гомоморфизма имеет ту же базовую функцию, что и f как отображение; т.е. сопоставление f сохраняет функцию.

LaTeX

$$$\\operatorname{toContinuousOrderHom}(f) = (f : \\alpha \\to \\beta) \\quad$ как отображение на множествах $\\alpha \\to \\beta$.$$

Lean4

@[simp]
theorem toContinuousOrderHom_coe {f : EsakiaHom α β} : f.toContinuousOrderHom = (f : α → β) :=
  rfl

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