case h.e'_3.h.e'_3.h.e'_3
α : Type u_2
β : Type u_1
γ : Type ?u.25458
δ : Type ?u.25461
ι : Type ?u.25464
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
f : β → Set α
hs : Set.Finite s
hfin : ∀ (i : β), i ∈ s → ↑↑μ (f i) ≠ ⊤
⊢ (fun i => ⋃ (_ : i ∈ s), f i) = fun b => ⋃ (_ : b ∈ Finite.toFinset hs), f b

case convert_3
α : Type u_2
β : Type u_1
γ : Type ?u.25458
δ : Type ?u.25461
ι : Type ?u.25464
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
f : β → Set α
hs : Set.Finite s
hfin : ∀ (i : β), i ∈ s → ↑↑μ (f i) ≠ ⊤
⊢ ∑ p in Finite.toFinset hs, ↑↑μ (f p) < ⊤
α : Type u_2
β : Type u_1
γ : Type ?u.25458
δ : Type ?u.25461
ι : Type ?u.25464
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
f : β → Set α
hs : Set.Finite s
hfin : ∀ (i : β), i ∈ s → ↑↑μ (f i) ≠ ⊤
⊢ ↑↑μ (⋃ (i : β) (_ : i ∈ s), f i) < ⊤
convert(measure_biUnion_finset_le hs.toFinset f).trans_lt _ using 3
case convert_3.h
α : Type u_2
β : Type u_1
γ : Type ?u.25458
δ : Type ?u.25461
ι : Type ?u.25464
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
f : β → Set α
hs : Set.Finite s
hfin : ∀ (i : β), i ∈ s → ↑↑μ (f i) ≠ ⊤
⊢ ∀ (a : β), a ∈ Finite.toFinset hs → ↑↑μ (f a) ≠ ⊤
case convert_3
α : Type u_2
β : Type u_1
γ : Type ?u.25458
δ : Type ?u.25461
ι : Type ?u.25464
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
f : β → Set α
hs : Set.Finite s
hfin : ∀ (i : β), i ∈ s → ↑↑μ (f i) ≠ ⊤
⊢ ∑ p in Finite.toFinset hs, ↑↑μ (f p) < ⊤
apply ENNReal.sum_lt_top
no goals
case convert_3.h
α : Type u_2
β : Type u_1
γ : Type ?u.25458
δ : Type ?u.25461
ι : Type ?u.25464
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
f : β → Set α
hs : Set.Finite s
hfin : ∀ (i : β), i ∈ s → ↑↑μ (f i) ≠ ⊤
⊢ ∀ (a : β), a ∈ Finite.toFinset hs → ↑↑μ (f a) ≠ ⊤
simpa only [Finite.mem_toFinset]
case h.e'_3.h.e'_3.h.e'_3.h.h
α : Type u_2
β : Type u_1
γ : Type ?u.25458
δ : Type ?u.25461
ι : Type ?u.25464
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
f : β → Set α
hs : Set.Finite s
hfin : ∀ (i : β), i ∈ s → ↑↑μ (f i) ≠ ⊤
x✝¹ : β
x✝ : α
⊢ (x✝ ∈ ⋃ (_ : x✝¹ ∈ s), f x✝¹) ↔ x✝ ∈ ⋃ (_ : x✝¹ ∈ Finite.toFinset hs), f x✝¹
case h.e'_3.h.e'_3.h.e'_3
α : Type u_2
β : Type u_1
γ : Type ?u.25458
δ : Type ?u.25461
ι : Type ?u.25464
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
f : β → Set α
hs : Set.Finite s
hfin : ∀ (i : β), i ∈ s → ↑↑μ (f i) ≠ ⊤
⊢ (fun i => ⋃ (_ : i ∈ s), f i) = fun b => ⋃ (_ : b ∈ Finite.toFinset hs), f b
ext
no goals
case h.e'_3.h.e'_3.h.e'_3.h.h
α : Type u_2
β : Type u_1
γ : Type ?u.25458
δ : Type ?u.25461
ι : Type ?u.25464
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
f : β → Set α
hs : Set.Finite s
hfin : ∀ (i : β), i ∈ s → ↑↑μ (f i) ≠ ⊤
x✝¹ : β
x✝ : α
⊢ (x✝ ∈ ⋃ (_ : x✝¹ ∈ s), f x✝¹) ↔ x✝ ∈ ⋃ (_ : x✝¹ ∈ Finite.toFinset hs), f x✝¹
rw [Finite.mem_toFinset]