no goals
α : Type u_1
β : Type ?u.885602
γ : Type ?u.885605
δ : Type ?u.885608
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
x : α
hx : ↑(restrict f s) x ≠ 0
hxs : x ∈ s
x✝ : ↑↑μ (↑(restrict f s) ⁻¹' {↑(restrict f s) x}) ≠ 0
⊢ ↑(restrict f s) x ∈ SimpleFunc.range f
simp only [f.restrict_apply hs, indicator_of_mem hxs, mem_range_self]
no goals
α : Type u_1
β : Type ?u.885602
γ : Type ?u.885605
δ : Type ?u.885608
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
x : α
hx : ↑(restrict f s) x ≠ 0
hxs : ¬x ∈ s
⊢ ↑(restrict f s) x = 0
simp [*]
no goals
α : Type u_1
β : Type ?u.885602
γ : Type ?u.885605
δ : Type ?u.885608
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
b : α
hb : ↑f b = 0
⊢ ↑f b * ↑↑μ (↑(restrict f s) ⁻¹' {↑f b}) = ↑f b * ↑↑μ (↑f ⁻¹' {↑f b} ∩ s)
simp only [hb, MulZeroClass.zero_mul]
no goals
α : Type u_1
β : Type ?u.885602
γ : Type ?u.885605
δ : Type ?u.885608
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
b : α
hb : ¬↑f b = 0
⊢ ↑f b * ↑↑μ (↑(restrict f s) ⁻¹' {↑f b}) = ↑f b * ↑↑μ (↑f ⁻¹' {↑f b} ∩ s)
rw [restrict_preimage_singleton _ hs hb, inter_comm]