map_mk_eq

Mathlib.Algebra.Order.Archimedean.Class

URI: https://scilib.ai/kg/mathlib#MulArchimedeanClass.map_mk_eq

English

If mk a = mk b, then mk (f a) = mk (f b) for any order-monoid hom f.

Русский

Если mk a = mk b, то mk (f a) = mk (f b) для любого ордерного моноидного гомоморфа f.

LaTeX

$$$(\\mk a = \\mk b) \\Rightarrow (\\mk (f a) = \\mk (f b))$$$

Lean4

@[to_additive]
theorem map_mk_eq (f : M →*o N) (h : mk a = mk b) : mk (f a) = mk (f b) := by rw [← orderHom_mk, ← orderHom_mk, h]

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

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

Разделы

Аффилиация

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