hom_ofHom — Mathlib

English

Let X and Y be frames and f a FrameHom X Y. Then the correspondingFrm morphism obtained from f has the same underlying map as f; i.e., the homomorphism component of Frm.ofHom f is exactly f.

Русский

Пусть X и Y — рамки и f : FrameHom X Y. Тогда соответствующий Frm-морфизм Frm.ofHom f имеет точно такое же отображение, как f; то есть компонент Frm.ofHom f .hom равен f.

LaTeX

$$$ (\mathrm{Frm}.ofHom(f)).\mathrm{hom} = f $$$

Lean4

@[simp]
theorem hom_ofHom {X Y : Type u} [Frame X] [Frame Y] (f : FrameHom X Y) : (ofHom f).hom = f :=
  rfl

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