lt_congr_right

Mathlib.Order.Antisymmetrization

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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