α : Type u_2
β : Type u_1
γ : Type ?u.4605823
δ : Type ?u.4605826
ι : Type ?u.4605829
R : Type ?u.4605832
R' : Type ?u.4605835
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
⊢ t ∈ Filter.map (indicator s f) (ae μ) → t ∈ Filter.map f (ae (Measure.restrict μ s))
α : Type u_2
β : Type u_1
γ : Type ?u.4605823
δ : Type ?u.4605826
ι : Type ?u.4605829
R : Type ?u.4605832
R' : Type ?u.4605835
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
⊢ Filter.map f (ae (Measure.restrict μ s)) ≤ Filter.map (indicator s f) (ae μ)
intro t
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.4605823
δ : Type ?u.4605826
ι : Type ?u.4605829
R : Type ?u.4605832
R' : Type ?u.4605835
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∈ t
⊢ t ∈ Filter.map (indicator s f) (ae μ) → t ∈ Filter.map f (ae (Measure.restrict μ s))

case neg
α : Type u_2
β : Type u_1
γ : Type ?u.4605823
δ : Type ?u.4605826
ι : Type ?u.4605829
R : Type ?u.4605832
R' : Type ?u.4605835
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : ¬0 ∈ t
⊢ t ∈ Filter.map (indicator s f) (ae μ) → t ∈ Filter.map f (ae (Measure.restrict μ s))
α : Type u_2
β : Type u_1
γ : Type ?u.4605823
δ : Type ?u.4605826
ι : Type ?u.4605829
R : Type ?u.4605832
R' : Type ?u.4605835
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
⊢ t ∈ Filter.map (indicator s f) (ae μ) → t ∈ Filter.map f (ae (Measure.restrict μ s))
by_cases ht : (0 : β) ∈ t
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.4605823
δ : Type ?u.4605826
ι : Type ?u.4605829
R : Type ?u.4605832
R' : Type ?u.4605835
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : ¬0 ∈ t
⊢ ↑↑μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0 → ↑↑μ ((f ⁻¹' t)ᶜ ∩ s) = 0
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.4605823
δ : Type ?u.4605826
ι : Type ?u.4605829
R : Type ?u.4605832
R' : Type ?u.4605835
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : ¬0 ∈ t
⊢ t ∈ Filter.map (indicator s f) (ae μ) → t ∈ Filter.map f (ae (Measure.restrict μ s))
rw [mem_map_indicator_ae_iff_of_zero_nmem ht, mem_map_restrict_ae_iff hs]
no goals
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.4605823
δ : Type ?u.4605826
ι : Type ?u.4605829
R : Type ?u.4605832
R' : Type ?u.4605835
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : ¬0 ∈ t
⊢ ↑↑μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0 → ↑↑μ ((f ⁻¹' t)ᶜ ∩ s) = 0
exact fun h => measure_mono_null ((Set.inter_subset_left _ _).trans (Set.subset_union_left _ _)) h
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.4605823
δ : Type ?u.4605826
ι : Type ?u.4605829
R : Type ?u.4605832
R' : Type ?u.4605835
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∈ t
⊢ t ∈ Filter.map f (ae (Measure.restrict μ s)) → t ∈ Filter.map f (ae (Measure.restrict μ s))
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.4605823
δ : Type ?u.4605826
ι : Type ?u.4605829
R : Type ?u.4605832
R' : Type ?u.4605835
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∈ t
⊢ t ∈ Filter.map (indicator s f) (ae μ) → t ∈ Filter.map f (ae (Measure.restrict μ s))
rw [mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem ht hs]
no goals
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.4605823
δ : Type ?u.4605826
ι : Type ?u.4605829
R : Type ?u.4605832
R' : Type ?u.4605835
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
t : Set β
ht : 0 ∈ t
⊢ t ∈ Filter.map f (ae (Measure.restrict μ s)) → t ∈ Filter.map f (ae (Measure.restrict μ s))
exact id