Sub_Basis_for_Real_Number_Line
Provedproofwikireal-numberstopological-bases
Let the real number line be considered as a topology under the usual (Euclidean) metric. Then is a sub-basis for .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Sub_Basis_for_Real_Number_Line : TopologicalSpace.IsTopologicalBasis (Set.range (fun p : ℝ × ℝ => Set.Ioo p.1 p.2)) := by sorry
Source