ofHom_id — Mathlib

English

For any frame X, the Frm image of the identity FrameHom on X is the identity on the object Frm.of X.

Русский

Для любого кадра X образ Frm от тождесного FrameHom на X равен тождественному морфизму на объекте Frm.of X.

LaTeX

$$$ \mathrm{ofHom}(\mathrm{FrameHom.id}(X)) = \mathbf{1}_{\mathrm{of}(X)} $$$

Lean4

@[simp]
theorem ofHom_id {X : Type u} [Frame X] : ofHom (FrameHom.id _) = 𝟙 (of X) :=
  rfl

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