pred_le_pred_iff_of_not_isMin — Mathlib

English

If a and b are not minimal, then pred a ≤ pred b iff a ≤ b.

Русский

Если a и b не минимальны, то pred(a) ≤ pred(b) эквивалентно a ≤ b.

LaTeX

$$$\neg\operatorname{IsMin}(a) \to (\neg\operatorname{IsMin}(b) \to (\operatorname{pred} a \le \operatorname{pred} b \iff a \le b))$$$

Lean4

theorem pred_le_pred_iff_of_not_isMin (ha : ¬IsMin a) (hb : ¬IsMin b) : pred a ≤ pred b ↔ a ≤ b := by
  rw [le_pred_iff_of_not_isMin hb, pred_lt_iff_of_not_isMin ha]

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