inr_mono

Mathlib.Data.Sum.Order

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

English

The right injection is monotone with respect to the sum order; if a ≤ b in β then inr(a) ≤ inr(b) in α ⊕ β.

Русский

Правая инъекция монотонна относительно порядка суммы: если a ≤ b в β, то inr(a) ≤ inr(b) в α ⊕ β.

LaTeX

$$$\forall a,b:\; a \le b \Rightarrow \mathrm{inr}(a) \le \mathrm{inr}(b)$$$

Lean4

theorem inr_mono : Monotone (inr : β → α ⊕ β) := fun _ _ => LiftRel.inr

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

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

Разделы

Аффилиация

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