inr_mono

Mathlib.Algebra.Order.Monoid.Lex

URI: https://scilib.ai/kg/mathlib#MonoidHom.inr_mono

English

The right injection x ↦ (1,x) is monotone: a ≤ b implies (1,a) ≤ (1,b).

Русский

Правая инъекция x ↦ (1,x) монотонна: a ≤ b ⇒ (1,a) ≤ (1,b).

LaTeX

$$a \le b \Rightarrow (1,a) \le (1,b)$$

Lean4

@[to_additive]
theorem inr_mono : Monotone (MonoidHom.inr α β) := fun _ _ ↦ by simp

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

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

Разделы

Аффилиация

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