Fixed discontinuities of laws on the Skorokhod space

A point-finite measurable family has only countably many members of positive measure. Apply this to jumps larger than a fixed threshold, then take a countable union.

theorem BGW.Skorokhod.countable_measure_ne_zero_of_point_finite {Ω : Type u_1} {I : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (A : I → Set Ω) (hA : ∀ (i : I), MeasurableSet (A i)) (hfin : ∀ (x : Ω), {i : I | x ∈ A i}.Finite) : {i : I | μ (A i) ≠ 0}.Countable

A point-finite measurable family has countably many members of positive finite measure.

theorem BGW.Skorokhod.countable_setOf_measure_jump_ne_zero {T : ℝ} {E : Type u_1} [MetricSpace E] [TopologicalSpace.SeparableSpace E] [MeasurableSpace E] [BorelSpace E] (P : MeasureTheory.ProbabilityMeasure (D T E)) : {t : ↑(Set.Icc 0 T) | ↑P {f : D T E | Function.leftLim (⇑f) t ≠ f t} ≠ 0}.Countable

A law on D has at most countably many fixed discontinuity times (C12(3)).