inr_le_inr_iff

Mathlib.Data.Sum.Order

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

English

For any a,b in β, (inr a) ≤ (inr b) in the sum iff a ≤ b in β.

Русский

Для любых a,b из β, (inr a) ≤ (inr b) в сумме эквивалентно a ≤ b в β.

LaTeX

$$$(\mathrm{inr}\,a) \le (\mathrm{inr}\,b) \iff a \le b$$$

Lean4

@[simp]
theorem inr_le_inr_iff [LE α] [LE β] {a b : β} : (inr a : α ⊕ β) ≤ inr b ↔ a ≤ b :=
  liftRel_inr_inr

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

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

Разделы

Аффилиация

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