English
A countable infimum of measurably generated filters is measurably generated.
Русский
Счётный инфимон порожденных измеримо сгенерированных фильтров является измеримо сгенерированным.
LaTeX
$$$\\\\forall {f : ι \\to Filter α}, [∀ i, IsMeasurablyGenerated (f i)] \\\\Rightarrow IsMeasurablyGenerated (\\\\inf i, f i)$$$
Lean4
instance iInf_isMeasurablyGenerated {f : ι → Filter α} [∀ i, IsMeasurablyGenerated (f i)] :
IsMeasurablyGenerated (⨅ i, f i) := by
refine ⟨fun s hs => ?_⟩
rw [← Equiv.plift.surjective.iInf_comp, mem_iInf] at hs
rcases hs with ⟨t, ht, ⟨V, hVf, rfl⟩⟩
choose U hUf hU using fun i => IsMeasurablyGenerated.exists_measurable_subset (hVf i)
refine ⟨⋂ i : t, U i, ?_, ?_, ?_⟩
· rw [← Equiv.plift.surjective.iInf_comp, mem_iInf]
exact ⟨t, ht, U, hUf, rfl⟩
· haveI := ht.countable.toEncodable.countable
exact MeasurableSet.iInter fun i => (hU i).1
· exact iInter_mono fun i => (hU i).2
