isClosed_Ioo_iff — Mathlib

English

For a < b in a densely ordered space with order topology, the open interval Ioo(a,b) is closed iff b ≤ a.

Русский

Для a < b в плотном линейно упорядоченном пространстве с топологией порядка, открытый интервал Ioo(a,b) замкнут тогда и только тогда, когда b ≤ a.

LaTeX

$$$\\operatorname{IsClosed}(\\mathrm{Ioo}(a,b)) \\iff b \\le a.$$$

Lean4

/-- `Set.Ioo a b` is only closed if it is empty. -/
@[simp]
theorem isClosed_Ioo_iff {a b : α} : IsClosed (Set.Ioo a b) ↔ b ≤ a :=
  by
  refine ⟨fun h => le_of_not_gt fun hab => ?_, by simp_all⟩
  have := h.closure_eq
  rw [closure_Ioo hab.ne, Icc_eq_Ioo_same_iff] at this
  exact this hab.le

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