le_congr_right

Mathlib.Order.Antisymmetrization

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

English

If b ≼ c in antisymmetry, 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 le_congr_right (h : AntisymmRel (· ≤ ·) b c) : a ≤ b ↔ a ≤ c :=
  AntisymmRel.rfl.le_congr h

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

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

Разделы

Аффилиация

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