withTopWithBot_id — Mathlib

English

The identity lattice homomorphism extended with top/bot equals the identity bounded lattice homomorphism on WithTop(WithBot α).

Русский

Тождественное отображение решётки, расширенное до WithTop(WithBot α), равно тождесвому ограниченному гомоморфизму на WithTop(WithBot α).

LaTeX

$$$ (\\mathrm{LatticeHom.id}\\, \\alpha).\\mathrm{withTopWithBot} = \\mathrm{BoundedLatticeHom.id}(\\mathrm{WithTop}(\\mathrm{WithBot}\\, \\alpha)) $$$

Lean4

@[simp]
theorem withTopWithBot_id : (LatticeHom.id α).withTopWithBot = BoundedLatticeHom.id _ :=
  DFunLike.coe_injective <| by simp [WithTop.map_id, WithBot.map_id]

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