inl_strictMono

Mathlib.Data.Sum.Order

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

English

The left injection is strictly monotone: a < b implies inl(a) < inl(b) in the sum.

Русский

Левая инъекция строго монотонна: a < b => inl(a) < inl(b).

LaTeX

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

Lean4

theorem inl_strictMono : StrictMono (inl : α → α ⊕ β) := fun _ _ => LiftRel.inl

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

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

Разделы

Аффилиация

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