wcovBy_of_eq_or_eq — Mathlib

English

If a ≤ b and for all c with a ≤ c ≤ b we have c = a or c = b, then a ⩿ b.

Русский

Если a ≤ b и для всех c с a ≤ c ≤ b имеем c = a или c = b, то a ⩿ b.

LaTeX

$$$a \\\\le b \\\\land (\\\\forall c, a \\\\le c \\\\to c \\\\le b \\\\to c = a \\\\lor c = b) \\\\Rightarrow a \\\\mathrel{\\\\trianglelefteq} b.$$$

Lean4

theorem wcovBy_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⟩

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