inr_le_inr_iff

Mathlib.Data.Sum.Order

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

English

For all a,b in β, toLex (inr a) ≤ toLex (inr b) holds iff a ≤ b.

Русский

Для всех a,b в β: toLex(inr a) ≤ toLex(inr b) эквивалентно a ≤ b.

LaTeX

$$$\forall a,b:\, a,b \in \beta:\; toLex(\mathrm{Sum.inr}(a)) \le toLex(\mathrm{Sum.inr}(b)) \iff a \le b.$$$

Lean4

theorem inr_le_inr_iff [LE α] [LE β] {a b : β} : toLex (inr a : α ⊕ β) ≤ toLex (inr b) ↔ a ≤ b :=
  lex_inr_inr

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

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

Разделы

Аффилиация

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