trans_antisymm_rel

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#WCovBy.trans_antisymm_rel

← MathLib Explorer

English

If a ⩿ b and AntisymmRel (≤) b c, then a ⩿ c.

Русский

Если a ⩿ b и AntisymmRel (≤) b c, то a ⩿ c.

LaTeX

$$$a \\\\mathrel{\\\\trianglelefteq} b \\\\land AntisymmRel (\\\\le) b c \\\\Rightarrow a \\\\mathrel{\\\\trianglelefteq} c.$$$

Lean4

theorem trans_antisymm_rel (hab : a ⩿ b) (hbc : AntisymmRel (· ≤ ·) b c) : a ⩿ c :=
  ⟨hab.le.trans hbc.1, fun _ had hdc => hab.2 had <| hdc.trans_le hbc.2⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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