wcovBy

Mathlib.Order.Cover

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

English

If a ≤ b and b ≤ a (antisymmetric relation), then a ⩿ b.

Русский

Если a ≤ b и b ≤ a (антисимметричность), то a ⩿ b.

LaTeX

$$$\\\\forall a,b, AntisymmRel (\\\\le) a b \\\\Rightarrow a \\\\mathrel{\\\\trianglelefteq} b.$$$

Lean4

theorem wcovBy (h : AntisymmRel (· ≤ ·) a b) : a ⩿ b :=
  wcovBy_of_le_of_le h.1 h.2

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

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

Разделы

Аффилиация

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