covBy_of_apply — Mathlib

English

If a and b are equivalent under ≤, then CovBy with left argument transfers: CovBy c a iff CovBy c b.

Русский

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

LaTeX

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

Lean4

theorem covBy_of_apply {α β : Type*} [Preorder α] [Preorder β] (f : α ↪o β) {x y : α} (h : f x ⋖ f y) : x ⋖ y :=
  by
  use f.lt_iff_lt.1 h.1
  intro a
  rw [← f.lt_iff_lt, ← f.lt_iff_lt]
  apply h.2

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