Set.Icc, Set.Ico, Set.Ici are not open in R

Stream: Is there code for X?

[Aaron Hill]

Is there a theorem that gives ¬ IsOpenfor the various closed/half-closed intervals, assuming that we're dealing with the real numbers with the usual topology?

[Ruben Van de Velde]

Not seeing anything obvious from a quick loogle search

[Ruben Van de Velde]

Here's one approach:

import Mathlib

example : ¬ IsOpen (Set.Icc (0 : ℝ) 1) := by
  rw [← interior_eq_iff_isOpen, Set.ext_iff, not_forall]
  use 1
  simp

[Bjørn Kjos-Hanssen]

Just remarking that Set.Icc a b is open if a>b.

example (a b : ℝ) (h : a ≤ b): ¬ IsOpen (Set.Icc a b) := by
  have : a ∈ Set.Icc a b := by simp;linarith
  have : ¬ b+1 ∈ Set.Icc a b := by simp
  have h₀: ¬ IsClopen (Set.Icc a b) := by
    rw [isClopen_iff]
    intro hc;cases hc <;> simp_all
  exact fun hc => h₀ ⟨isClosed_Icc,hc⟩