trans_wcovBy — Mathlib

English

If a ⩿ b and b ⩿ c, then a ⩿ c (transitivity of the covering relation).

Русский

Если a ⩿ b и b ⩿ c, тогда a ⩿ c (транзитивность).

LaTeX

$$$a \\\\mathrel{\\\\trianglelefteq} b \\\\land b \\\\mathrel{\\\\trianglelefteq} c \\\\Rightarrow a \\\\mathrel{\\\\trianglelefteq} c.$$$

Lean4

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

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