English
For any x and sets t,s, the measure of the piecewise-set is μ(if x∈t then s else ∅) = 1_t(x) μ(s).
Русский
Для любых x и множеств t,s выполняется μ(если x∈t, то s, иначе ∅) = 1_t(x) μ(s).
LaTeX
$$$$\mu\bigl(\text{if } x \in t \text{ then } s \text{ else } \emptyset\bigr) = \mathbf{1}_t(x) \cdot \mu(s).$$$$
Lean4
/-- The measure of the intersection of a decreasing sequence of measurable
sets indexed by a linear order with first countable topology is the limit of the measures. -/
theorem tendsto_measure_biInter_gt {ι : Type*} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [DenselyOrdered ι]
[FirstCountableTopology ι] {s : ι → Set α} {a : ι} (hs : ∀ r > a, NullMeasurableSet (s r) μ)
(hm : ∀ i j, a < i → i ≤ j → s i ⊆ s j) (hf : ∃ r > a, μ (s r) ≠ ∞) :
Tendsto (μ ∘ s) (𝓝[Ioi a] a) (𝓝 (μ (⋂ r > a, s r))) :=
by
have : (atBot : Filter (Ioi a)).IsCountablyGenerated :=
by
rw [← comap_coe_Ioi_nhdsGT]
infer_instance
simp_rw [← map_coe_Ioi_atBot, tendsto_map'_iff, ← mem_Ioi, biInter_eq_iInter]
apply tendsto_measure_iInter_atBot
· rwa [Subtype.forall]
· exact fun i j h ↦ hm i j i.2 h
· simpa only [Subtype.exists, exists_prop]
