covBy_of_eq_or_eq — Mathlib

English

If a < b and for every c with a ≤ c ≤ b, c is either a or b, then a ⋖ b.

Русский

Если a < b и для каждого c, с a ≤ c ≤ b, имеет место c = a или c = b, тогда a ⋖ b.

LaTeX

$$$ (a < b) \\land (\\forall c, a \\le c \\to c \\le b \\to (c = a \\lor c = b)) \\Rightarrow a \\,⋖\\, b $$$

Lean4

theorem covBy_of_eq_or_eq (hab : a < b) (h : ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b) : a ⋖ b :=
  ⟨hab, fun c ha hb => (h c ha.le hb.le).elim ha.ne' hb.ne⟩

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