inf_isMeasurablyGenerated — Mathlib

English

The infimum of two measurably generated filters is measurably generated.

Русский

Пересечение двух измеримо порожденных фильтров является измеримо порожденным.

LaTeX

$$$\\\\forall {f g : Filter α}, [IsMeasurablyGenerated f] [IsMeasurablyGenerated g] \\\\Rightarrow IsMeasurablyGenerated (f \\\\inf g)$$$

Lean4

instance inf_isMeasurablyGenerated (f g : Filter α) [IsMeasurablyGenerated f] [IsMeasurablyGenerated g] :
    IsMeasurablyGenerated (f ⊓ g) := by
  constructor
  rintro t ⟨sf, hsf, sg, hsg, rfl⟩
  rcases IsMeasurablyGenerated.exists_measurable_subset hsf with ⟨s'f, hs'f, hmf, hs'sf⟩
  rcases IsMeasurablyGenerated.exists_measurable_subset hsg with ⟨s'g, hs'g, hmg, hs'sg⟩
  refine ⟨s'f ∩ s'g, inter_mem_inf hs'f hs'g, hmf.inter hmg, ?_⟩
  exact inter_subset_inter hs'sf hs'sg

Похожие утверждения