trans_covBy — Mathlib

English

If a and b are equivalent under ≤ (AntisymmRel) and b covers c, then a covers c.

Русский

Если a и b эквивалентны относительно ≤, и b покрывает c, то a покрывает c.

LaTeX

$$$ (\\text{AntisymmRel}(\\le)\\ a\\ b) \\land (b \\,⋖\\, c) \\Rightarrow a \\,⋖\\, c $$$

Lean4

theorem trans_covBy (hab : AntisymmRel (· ≤ ·) a b) (hbc : b ⋖ c) : a ⋖ c :=
  ⟨hab.1.trans_lt hbc.lt, fun _ had hdc => hbc.2 (hab.2.trans_lt had) hdc⟩

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