α : Type u_2
β : Type u_1
ι : Type ?u.1439544
E : Type ?u.1439547
F : Type ?u.1439550
𝕜 : Type ?u.1439553
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
inst✝ : Zero β
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
⊢ ↑↑μ (⋃ (y : β) (_ : y ∈ filter (fun y => y ≠ 0) (SimpleFunc.range f)), ↑f ⁻¹' {y}) < ⊤
α : Type u_2
β : Type u_1
ι : Type ?u.1439544
E : Type ?u.1439547
F : Type ?u.1439550
𝕜 : Type ?u.1439553
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
inst✝ : Zero β
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
⊢ ↑↑μ (support ↑f) < ⊤
rw [support_eq]
α : Type u_2
β : Type u_1
ι : Type ?u.1439544
E : Type ?u.1439547
F : Type ?u.1439550
𝕜 : Type ?u.1439553
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
inst✝ : Zero β
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
y : β
hy : y ∈ filter (fun y => y ≠ 0) (SimpleFunc.range f)
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
α : Type u_2
β : Type u_1
ι : Type ?u.1439544
E : Type ?u.1439547
F : Type ?u.1439550
𝕜 : Type ?u.1439553
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
inst✝ : Zero β
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
⊢ ↑↑μ (⋃ (y : β) (_ : y ∈ filter (fun y => y ≠ 0) (SimpleFunc.range f)), ↑f ⁻¹' {y}) < ⊤
refine' (measure_biUnion_finset_le _ _).trans_lt (ENNReal.sum_lt_top_iff.mpr fun y hy => _)
α : Type u_2
β : Type u_1
ι : Type ?u.1439544
E : Type ?u.1439547
F : Type ?u.1439550
𝕜 : Type ?u.1439553
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
inst✝ : Zero β
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
y : β
hy : y ∈ SimpleFunc.range f ∧ y ≠ 0
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
α : Type u_2
β : Type u_1
ι : Type ?u.1439544
E : Type ?u.1439547
F : Type ?u.1439550
𝕜 : Type ?u.1439553
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
inst✝ : Zero β
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
y : β
hy : y ∈ filter (fun y => y ≠ 0) (SimpleFunc.range f)
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
rw [Finset.mem_filter] at hy
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.1439544
E : Type ?u.1439547
F : Type ?u.1439550
𝕜 : Type ?u.1439553
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
inst✝ : Zero β
f : α →ₛ β
hf : ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
y : β
hy : y ∈ SimpleFunc.range f ∧ y ≠ 0
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
exact hf y hy.2