inl_mono

Mathlib.Data.Sum.Order

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

English

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

Русский

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

LaTeX

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

Lean4

theorem inl_mono : Monotone (inl : α → α ⊕ β) := fun _ _ => LiftRel.inl

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

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

Разделы

Аффилиация

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