coe_mk — Mathlib

English

The constructor mk yields a BoundedLatticeHom whose underlying function is f and whose top/bot maps match given hf and hf'.

Русский

Конструктор mk порождает BoundedLatticeHom, чья базовая функция равна f, а отображения top/bot заданы hf, hf'.

LaTeX

$$$\\forall f:\\mathrm{LatticeHom}(\\alpha,\\beta),\\ \\forall hf:\\ f\\top = top,\\ hf': f\\bot = bot \\Rightarrow \\text{mk}(f, hf, hf')\\text{ yields a }\\mathrm{BoundedLatticeHom}$$$

Lean4

@[simp]
theorem coe_mk (f : LatticeHom α β) (hf hf') : ⇑(mk f hf hf') = f :=
  rfl

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