pred_le_of_wcovBy — Mathlib

English

For any a and b with a ⩿ b, pred(b) ≤ a.

Русский

Для любых a и b с a ⩿ b, pred(b) ≤ a.

LaTeX

$$$ (a \ntriangleright b) \Rightarrow pred(b) \le a $$$

Lean4

/-- See also `Order.pred_eq_of_covBy`. -/
theorem pred_le_of_wcovBy (h : a ⩿ b) : pred b ≤ a :=
  by
  obtain hab | ⟨-, hba⟩ := h.covBy_or_le_and_le
  · by_contra hba
    exact h.2 (hab.lt.le_pred.lt_of_not_ge hba) (pred_lt_of_not_isMin hab.lt.not_isMin)
  · exact (pred_le _).trans hba

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