trans_antisymmRel

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#CovBy.trans_antisymmRel

← MathLib Explorer

English

If a is covBy b and b is related to c by AntisymmRel, then a is covBy c.

Русский

Если a ⋖ b и b связан с c через AntisymmRel, то a ⋖ c.

LaTeX

$$$ (a \\⋖\\, b) \\land (hbc : AntisymmRel(\\le) b c) \\Rightarrow a \\,⋖\\, c $$$

Lean4

theorem trans_antisymmRel (hab : a ⋖ b) (hbc : AntisymmRel (· ≤ ·) b c) : a ⋖ c :=
  ⟨hab.lt.trans_le hbc.1, fun _ had hdb => hab.2 had <| hdb.trans_le hbc.2⟩

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

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

Разделы

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

Аффилиация

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