case mp
α : Type u_1
β : Type u_2
γ : Type ?u.906136
δ : Type ?u.906139
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
⊢ SimpleFunc.FinMeasSupp f μ → ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤

case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.906136
δ : Type ?u.906139
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
⊢ (∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤) → SimpleFunc.FinMeasSupp f μ
α : Type u_1
β : Type u_2
γ : Type ?u.906136
δ : Type ?u.906139
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
⊢ SimpleFunc.FinMeasSupp f μ ↔ ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
constructor
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.906136
δ : Type ?u.906139
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
h : SimpleFunc.FinMeasSupp f μ
y : β
hy : y ≠ 0
⊢ ↑f ⁻¹' {y} ⊆ {x | (fun x => ↑f x = OfNat.ofNat 0 x) x}ᶜ
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.906136
δ : Type ?u.906139
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
⊢ SimpleFunc.FinMeasSupp f μ → ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
refine' fun h y hy => lt_of_le_of_lt (measure_mono _) h
no goals
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.906136
δ : Type ?u.906139
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
h : SimpleFunc.FinMeasSupp f μ
y : β
hy : y ≠ 0
⊢ ↑f ⁻¹' {y} ⊆ {x | (fun x => ↑f x = OfNat.ofNat 0 x) x}ᶜ
exact fun x hx (H : f x = 0) => hy <| H ▸ Eq.symm hx
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.906136
δ : Type ?u.906139
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
H : ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
⊢ SimpleFunc.FinMeasSupp f μ
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.906136
δ : Type ?u.906139
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
⊢ (∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤) → SimpleFunc.FinMeasSupp f μ
intro H
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.906136
δ : Type ?u.906139
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
H : ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
⊢ ↑↑μ (⋃ (y : β) (_ : y ∈ filter (fun y => y ≠ 0) (SimpleFunc.range f)), ↑f ⁻¹' {y}) < ⊤
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.906136
δ : Type ?u.906139
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
H : ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
⊢ SimpleFunc.FinMeasSupp f μ
rw [finMeasSupp_iff_support, support_eq]
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.906136
δ : Type ?u.906139
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
H : ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
⊢ ∀ (a : β), a ∈ filter (fun y => y ≠ 0) (SimpleFunc.range f) → ↑↑μ (↑f ⁻¹' {a}) ≠ ⊤
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.906136
δ : Type ?u.906139
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
H : ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
⊢ ↑↑μ (⋃ (y : β) (_ : y ∈ filter (fun y => y ≠ 0) (SimpleFunc.range f)), ↑f ⁻¹' {y}) < ⊤
refine' lt_of_le_of_lt (measure_biUnion_finset_le _ _) (sum_lt_top _)
no goals
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.906136
δ : Type ?u.906139
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
H : ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
⊢ ∀ (a : β), a ∈ filter (fun y => y ≠ 0) (SimpleFunc.range f) → ↑↑μ (↑f ⁻¹' {a}) ≠ ⊤
exact fun y hy => (H y (Finset.mem_filter.1 hy).2).ne