isClosed_Ioc_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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