Set_of_All_Real_Intervals_is_Semiring_of_Sets
Provedmeasure-theoryproofwikireal-analysis
The set of all real intervals is a semiring of sets, but not a ring of sets.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Set_of_All_Real_Intervals_is_Semiring_of_Sets : ∀ a b c d : ℝ, a ≤ b → c ≤ d → ∃ e f : ℝ, Set.Icc a b ∩ Set.Icc c d = Set.Icc e f := by sorry
Source