An open interval neighborhood of a closed interval in an open set

Proved

BianchiIX.exists_Ioo_covering_Icc

by trppppp · Nov 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

bianchi-ix-era-statisticsdynamical-systems

If $s\leq t$ , $U\subset\mathbb R$ is open, and $[s,t]\subset U$ , then there are $l<s$ and $r>t$ such that $(l,r)\subset U$ .

Preamble

import Mathlib.Topology.Instances.Real.Lemmas
import Mathlib.Tactic.Linarith

namespace BianchiIX
end BianchiIX

noncomputable section
open BianchiIX
open Set Filter
open scoped Topology

Formal statement

theorem BianchiIX.exists_Ioo_covering_Icc {s t : ℝ} {U : Set ℝ} (hst : s ≤ t)
    (hU : IsOpen U) (hsub : Icc s t ⊆ U) :
    ∃ l r : ℝ, l < s ∧ t < r ∧ Ioo l r ⊆ U := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Analysis/IntervalNeighborhood.lean#L11-L25

View graph