withBot_id — Mathlib

English

Let α be a lattice. The identity lattice homomorphism on α, when extended with bottom, is the identity on WithBot α.

Русский

Пусть α — решётка. Отображение-тождество на α, продолженное добавлением нижней границы, является тождеством на WithBot α.

LaTeX

$$$ (\\mathrm{LatticeHom}.id\\, \\alpha).\\mathrm{withBot} = \\mathrm{LatticeHom}.id\\ (\\mathrm{WithBot}\\ \\alpha) $$$

Lean4

@[simp]
theorem withBot_id : (LatticeHom.id α).withBot = LatticeHom.id _ :=
  DFunLike.coe_injective WithBot.map_id

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