inl_le_inl_iff

Mathlib.Data.Sum.Order

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

English

For all a,b in α, toLex (inl a) ≤ toLex (inl b) holds iff a ≤ b.

Русский

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

LaTeX

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

Lean4

theorem inl_le_inl_iff [LE α] [LE β] {a b : α} : toLex (inl a : α ⊕ β) ≤ toLex (inl b) ↔ a ≤ b :=
  lex_inl_inl

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

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

Разделы

Аффилиация

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