inr_strictMono

Mathlib.Data.Sum.Order

URI: https://scilib.ai/kg/mathlib#Sum.Lex.inr_strictMono

English

The map toLex ∘ inr is strictly monotone; right injection into the lexicographic sum preserves order strictly.

Русский

Вложение справа в лексикографическую сумму через toLex строго монотонно.

LaTeX

$$$\\text{StrictMono}(\\text{toLex} \\circ \\text{inr})$$$

Lean4

theorem inr_strictMono : StrictMono (toLex ∘ inr : β → α ⊕ₗ β) :=
  toLex_strictMono.comp Sum.inr_strictMono

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

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

Разделы

Аффилиация

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