mk_inj

Mathlib.Data.PFunctor.Univariate.M

URI: https://scilib.ai/kg/mathlib#PFunctor.M.mk_inj

English

M.mk is injective: if M.mk x = M.mk y then x = y.

Русский

M.mk инъективен: если M.mk x = M.mk y, то x = y.

LaTeX

$$$\\forall {F : \\text{PFunctor}} \\{x y : F.Obj F.M\\},\\; M.mk x = M.mk y \\Rightarrow x = y$$$

Lean4

theorem mk_inj {x y : F (M F)} (h : M.mk x = M.mk y) : x = y := by rw [← dest_mk x, h, dest_mk]

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

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

Разделы

Аффилиация

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