apply_covBy_apply_iff — Mathlib

English

If a and b are equivalent under ≤, then CovBy with c is preserved: a ⋖ c iff b ⋖ c.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem apply_covBy_apply_iff {E : Type*} [EquivLike E α β] [OrderIsoClass E α β] (e : E) : e a ⋖ e b ↔ a ⋖ b :=
  (ordConnected_range (e : α ≃o β)).apply_covBy_apply_iff ((e : α ≃o β) : α ↪o β)

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