There exists a countable dense subset of nonnegative real time containing zero

Proved

AvramDividend.Classical.exists_countable_dense_nnreal_time_set_zero

by WillR · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

avram-classicalcountabledense-setnonnegative-timestopping-times

There is a countable dense subset S of the time domain ℝ≥0 that contains its bottom element zero. Apply Mathlib's Dense.exists_countable_dense_subset_bot_top to the whole separable space ℝ≥0. This eliminates the extrinsic dense sampling set assumption from the accepted reflected continuous-time prefix supremum adaptedness theorem and from the forthcoming true capped first closed-level hitting stopping-time theorem. It is an existence theorem only: the family can be chosen once and used uniformly for all time horizons and thresholds.

Preamble

import Definitions.Def_AvramDividend_Classical_SpectrallyNegativeLevy
import Mathlib.Topology.Bases
import Mathlib.Data.NNReal.Basic
import Mathlib.Order.BoundedOrder.Basic

open AvramDividend.Classical Set Topology
open scoped NNReal

Formal statement

theorem AvramDividend.Classical.exists_countable_dense_nnreal_time_set_zero :
    ∃ S : Set ℝ≥0,
      S.Countable ∧ Dense S ∧ (0 : ℝ≥0) ∈ S := by sorry

Source

Pinned Mathlib.Topology.Bases Dense.exists_countable_dense_subset_bot_top; Mathlib.Order.BoundedOrder.Basic isBot_bot.

View graph