withBot_id — Mathlib

English

Identity extension to bottom via SupHom coincides with the canonical bottom-extension identity.

Русский

Расширение книзу для тождественного отображения SupHom совпадает с каноническим тождественным отображением на WithBot.

LaTeX

$$$ (\mathrm{SupHom.id}\ \alpha).{\mathrm{withBot}} = \mathrm{SupBotHom.id}\ (\mathrm{WithBot}\ \alpha) $$$

Lean4

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

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