covBy_iff_lt_and_eq_or_eq — Mathlib

English

An equivalence: a ⋖ b iff a < b and every c with a ≤ c ≤ b satisfies c = a or c = b.

Русский

Эквивалентность: a ⋖ b тогда и только тогда, когда a < b и для каждого c с a ≤ c ≤ b выполняется c = a или c = b.

LaTeX

$$$a \lt b \;\land\; \forall c,\ a \le c \rightarrow c \le b \rightarrow (c = a \lor c = b) \\iff a \mathrm{CovBy} \ b$$

Lean4

/-- An `iff` version of `CovBy.eq_or_eq` and `covBy_of_eq_or_eq`. -/
theorem covBy_iff_lt_and_eq_or_eq : a ⋖ b ↔ a < b ∧ ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b :=
  ⟨fun h => ⟨h.lt, fun _ => h.eq_or_eq⟩, And.rec covBy_of_eq_or_eq⟩

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