mem_map_indicator_ae_iff_of_zero_notMem

English

If 0 is not in t, then membership in the mapped ae-set equals a measure condition on the preimage

Русский

Если 0 не принадлежит t, то принадлежность t в отображении ae эквивалентна условию по предобразу

LaTeX

$$$ t \\in \\operatorname{map}(s.indicator f) (ae \\mu) \\iff \\mu((f^{-1}(t))^c \\cup s^c) = 0 $$$

Lean4

theorem mem_map_indicator_ae_iff_of_zero_notMem [Zero β] {t : Set β} (ht : (0 : β) ∉ t) :
    t ∈ Filter.map (s.indicator f) (ae μ) ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0 := by
  classical
  rw [mem_map, mem_ae_iff, Set.indicator_preimage, Set.ite, Set.compl_union, Set.compl_inter]
  change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun _ => (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0
  simp only [ht, if_false, Set.compl_empty, Set.empty_diff, Set.inter_univ, Set.preimage_const]

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