Intervals cut out by a finite set of real values
DefinitionEsgk_FiniteRealCutIntervalsorder-theoryreal-analysis
This assigns to each optional cut point the portion of a real set lying before the first cut or between that cut and the next larger cut.
Definition code
-- Extracted dependency interfaces and their necessary proofs.
import Mathlib
/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/
noncomputable section
open Set
open scoped Classical
namespace Esgk
def realCutInterval (J : Set ℝ) (T : Finset ℝ) : Option {t // t ∈ T} → Set ℝ
| none => {x | x ∈ J ∧ ∀ t ∈ T, x < t}
| some c => {x | x ∈ J ∧ (c : ℝ) < x ∧ ∀ t ∈ T, (c : ℝ) < t → x < t}
end Esgk