lt_congr_left

Mathlib.Order.Antisymmetrization

URI: https://scilib.ai/kg/mathlib#AntisymmRel.lt_congr_left

English

If a ≼ b, then a < c ↔ b < c for any c.

Русский

Если a ≼ b, тогда a < c эквивалентно b < c.

LaTeX

$$$\\forall a,b,c \\in α,\\ AntisymmRel(≤) a b \\to (a < c) \\leftrightarrow (b < c)$$$

Lean4

theorem lt_congr_left (h : AntisymmRel (· ≤ ·) a b) : a < c ↔ b < c :=
  h.lt_congr .rfl

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

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

Разделы

Аффилиация

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