antisymmRel_congr_right

Mathlib.Order.Antisymmetrization

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

English

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

Русский

Если b ≼ c, тогда a ≼ b ↔ a ≼ c для любого a.

LaTeX

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

Lean4

theorem antisymmRel_congr_right (h : AntisymmRel (· ≤ ·) b c) : AntisymmRel (· ≤ ·) a b ↔ AntisymmRel (· ≤ ·) a c :=
  rel_congr_right h

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

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

Разделы

Аффилиация

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