English
Define on α the σ-algebra of sets that are measurable up to the σ-filter l, i.e., a set is measurable if it is eventually equal (mod l) to a measurable set.
Русский
Задаётся σ-алгебра множества на α, состоящая из множест, которые измеримы относительно заданного σ-фильтра l, то есть s измеримо ⇔ существует t измеримое и s ≡⟂l t.
LaTeX
$$$\text{MeasurableSet}'(s) := ∃ t, \mathrm{MeasurableSet}(t) ∧ s =^l t.$$$
Lean4
/-- The `MeasurableSpace` of sets which are measurable with respect to a given σ-algebra `m`
on `α`, modulo a given σ-filter `l` on `α`. -/
def eventuallyMeasurableSpace (l : Filter α) [CountableInterFilter l] : MeasurableSpace α
where
MeasurableSet' s := ∃ t, MeasurableSet t ∧ s =ᶠ[l] t
measurableSet_empty := ⟨∅, MeasurableSet.empty, EventuallyEq.refl _ _⟩
measurableSet_compl := fun _ ⟨t, ht, hts⟩ => ⟨tᶜ, ht.compl, hts.compl⟩
measurableSet_iUnion s
hs := by
choose t ht hts using hs
exact ⟨⋃ i, t i, MeasurableSet.iUnion ht, EventuallyEq.countable_iUnion hts⟩
