`BookProof.ChapterSelectingEvents.finite_set_null_in_continuous` {α : Type*} [MeasurableSpace α] (μ : Measure α) [NullSingletonClass μ] (s : Finset α) : μ (s : Set α) = 0

Proved

BookProof.ChapterSelectingEvents.finite_set_null_in_continuous

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterSelectingEvents.

BookProof.ChapterSelectingEvents.finite_set_null_in_continuous {α : Type*} [MeasurableSpace α] (μ : Measure α) [NullSingletonClass μ] (s : Finset α) : μ (s : Set α) = 0

Formalization note: Lean 4 identifier BookProof.ChapterSelectingEvents.finite_set_null_in_continuous.

Preamble

-- Generated from ChapterSelectingEvents.lean — theorem BookProof.ChapterSelectingEvents.finite_set_null_in_continuous
import Mathlib
import Definitions.Def_ChapterSelectingEvents
open BookProof.ChapterSelectingEvents


open scoped BigOperators
open MeasureTheory ProbabilityTheory


variable (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]

Formal statement

theorem BookProof.ChapterSelectingEvents.finite_set_null_in_continuous {α : Type*} [MeasurableSpace α]
    (μ : Measure α) [NullSingletonClass μ] (s : Finset α) : μ (s : Set α) = 0 := by sorry

View graph