hom_ext

Mathlib.Order.Category.Frm

URI: https://scilib.ai/kg/mathlib#Frm.hom_ext

English

The Frm ext lemma states that two Frm morphisms are equal if their underlying FrameHom components are equal.

Русский

Лемма экстенсиональности Frm говорит, что два морфизма Frm равны, если их компоненты FrameHom равны.

LaTeX

$$$ f.hom = g.hom \\Rightarrow f = g $$$

Lean4

@[ext]
theorem hom_ext {X Y : Frm} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g :=
  Hom.ext hf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru