le_iff_lt_or_antisymmRel

Mathlib.Order.Antisymmetrization

URI: https://scilib.ai/kg/mathlib#le_iff_lt_or_antisymmRel

English

For any a,b in a preorder, a ≤ b if and only if either a < b or AntisymmRel (≤) a b.

Русский

Для любых a,b в предпорядке: a ≤ b тогда и только если либо a < b, либо AntisymmRel (≤) a b.

LaTeX

$$$a \le b \iff a < b \lor \mathrm{AntisymmRel}(\le)\,a\,b$$$

Lean4

theorem le_iff_lt_or_antisymmRel : a ≤ b ↔ a < b ∨ AntisymmRel (· ≤ ·) a b :=
  by
  rw [lt_iff_le_not_ge, AntisymmRel]
  tauto

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

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

Разделы

Аффилиация

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