Ioo_eq_empty_iff_pred_le — Mathlib

English

Ioo a b is empty if and only if pred b ≤ a.

Русский

Ioo a b пусто тогда и только тогда, когда pred b ≤ a.

LaTeX

$$$ Ioo a b = \\emptyset \\iff \\mathrm{pred}\\ b \\le a $$$

Lean4

@[simp]
theorem Ioo_eq_empty_iff_pred_le : Ioo a b = ∅ ↔ pred b ≤ a :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · contrapose! h
    exact ⟨pred b, h, pred_lt_iff_not_isMin.mpr (not_isMin b)⟩
  · ext x
    suffices a < x → b ≤ x by simpa
    exact fun hx ↦ le_of_pred_lt <| lt_of_le_of_lt h hx

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