α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
⊢ ↑v a ≤ ↑w a
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
⊢ restrict v (⋃ (n : ℕ), f n) ≤ restrict w (⋃ (n : ℕ), f n)
refine' restrict_le_restrict_of_subset_le v w fun a ha₁ ha₂ => _
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
⊢ ↑v a ≤ ↑w a
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
⊢ ↑v a ≤ ↑w a
have ha₃ : (⋃ n, a ∩ disjointed f n) = a := by
  rwa [← Set.inter_iUnion, iUnion_disjointed, Set.inter_eq_left_iff_subset]
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ ↑v a ≤ ↑w a
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
⊢ ↑v a ≤ ↑w a
have ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n) :=
  (disjoint_disjointed _).mono fun i j => Disjoint.mono inf_le_right inf_le_right
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ (∑' (i : ℕ), ↑v (a ∩ disjointed f i)) ≤ ∑' (i : ℕ), ↑w (a ∩ disjointed f i)

α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ ∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)

α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ ∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ ↑v a ≤ ↑w a
rw [← ha₃, v.of_disjoint_iUnion_nat _ ha₄, w.of_disjoint_iUnion_nat _ ha₄]
case refine'_1
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
n : ℕ
⊢ MeasurableSet (a ∩ disjointed f n)

case refine'_2
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
n : ℕ
⊢ a ∩ disjointed f n ⊆ f n

case refine'_3
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ Summable fun i => ↑v (a ∩ disjointed f i)

case refine'_4
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ Summable fun i => ↑w (a ∩ disjointed f i)

α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ ∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)

α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ ∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ (∑' (i : ℕ), ↑v (a ∩ disjointed f i)) ≤ ∑' (i : ℕ), ↑w (a ∩ disjointed f i)

α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ ∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)

α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ ∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)
refine' tsum_le_tsum (fun n => (restrict_le_restrict_iff v w (hf₁ n)).1 (hf₂ n) _ _) _ _
no goals
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
⊢ (⋃ (n : ℕ), a ∩ disjointed f n) = a
rwa [← Set.inter_iUnion, iUnion_disjointed, Set.inter_eq_left_iff_subset]
no goals
case refine'_1
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
n : ℕ
⊢ MeasurableSet (a ∩ disjointed f n)
exact ha₁.inter (MeasurableSet.disjointed hf₁ n)
no goals
case refine'_2
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
n : ℕ
⊢ a ∩ disjointed f n ⊆ f n
exact Set.Subset.trans (Set.inter_subset_right _ _) (disjointed_subset _ _)
case refine'_3.refine'_1
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
n : ℕ
⊢ MeasurableSet (a ∩ disjointed f n)

case refine'_3.refine'_2
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ Pairwise (Disjoint on fun i => a ∩ disjointed f i)
case refine'_3
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ Summable fun i => ↑v (a ∩ disjointed f i)
refine' (v.m_iUnion (fun n => _) _).summable
no goals
case refine'_3.refine'_1
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
n : ℕ
⊢ MeasurableSet (a ∩ disjointed f n)
exact ha₁.inter (MeasurableSet.disjointed hf₁ n)
no goals
case refine'_3.refine'_2
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ Pairwise (Disjoint on fun i => a ∩ disjointed f i)
exact (disjoint_disjointed _).mono fun i j => Disjoint.mono inf_le_right inf_le_right
case refine'_4.refine'_1
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
n : ℕ
⊢ MeasurableSet (a ∩ disjointed f n)

case refine'_4.refine'_2
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ Pairwise (Disjoint on fun i => a ∩ disjointed f i)
case refine'_4
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ Summable fun i => ↑w (a ∩ disjointed f i)
refine' (w.m_iUnion (fun n => _) _).summable
no goals
case refine'_4.refine'_1
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
n : ℕ
⊢ MeasurableSet (a ∩ disjointed f n)
exact ha₁.inter (MeasurableSet.disjointed hf₁ n)
no goals
case refine'_4.refine'_2
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ Pairwise (Disjoint on fun i => a ∩ disjointed f i)
exact (disjoint_disjointed _).mono fun i j => Disjoint.mono inf_le_right inf_le_right
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
n : ℕ
⊢ MeasurableSet (a ∩ disjointed f n)
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ ∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)
intro n
no goals
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
n : ℕ
⊢ MeasurableSet (a ∩ disjointed f n)
exact ha₁.inter (MeasurableSet.disjointed hf₁ n)
no goals
α : Type u_1
β : Type ?u.555378
m : MeasurableSpace α
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), restrict v (f n) ≤ restrict w (f n)
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ (n : ℕ), f n
ha₃ : (⋃ (n : ℕ), a ∩ disjointed f n) = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ ∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)
exact fun n => ha₁.inter (MeasurableSet.disjointed hf₁ n)