le_succ_of_wcovBy — Mathlib

English

If a is weakly covered by b, then b ≤ succ(a).

Русский

Если a слабно покрывается b, то b ≤ succ(a).

LaTeX

$$$a \\mathrel{\\mathrm{WCovBy}} b \\Rightarrow b \\le \\operatorname{succ}(a)$$$

Lean4

/-- See also `Order.succ_eq_of_covBy`. -/
theorem le_succ_of_wcovBy (h : a ⩿ b) : b ≤ succ a :=
  by
  obtain hab | ⟨-, hba⟩ := h.covBy_or_le_and_le
  · by_contra hba
    exact h.2 (lt_succ_of_not_isMax hab.lt.not_isMax) <| hab.lt.succ_le.lt_of_not_ge hba
  · exact hba.trans (le_succ _)

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