isClosed_Ico_iff — Mathlib

English

For a < b in a densely ordered space with order topology, the half-open interval Ico(a,b) is closed if and only if b ≤ a.

Русский

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

LaTeX

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

Lean4

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

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