α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
⊢ (∑' (i : ℕ), ↑m (s i)) ≤ ↑m (⋃ (i : ℕ), s i)
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
⊢ ↑m (⋃ (i : ℕ), s i) = ∑' (i : ℕ), ↑m (s i)
refine' le_antisymm (m.iUnion_nat s) _
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
⊢ (⨆ (i : ℕ), ∑ a in Finset.range i, ↑m (s a)) ≤ ↑m (⋃ (i : ℕ), s i)
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
⊢ (∑' (i : ℕ), ↑m (s i)) ≤ ↑m (⋃ (i : ℕ), s i)
rw [ENNReal.tsum_eq_iSup_nat]
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
⊢ ∑ a in Finset.range n, ↑m (s a) ≤ ↑m (⋃ (i : ℕ), s i)
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
⊢ (⨆ (i : ℕ), ∑ a in Finset.range i, ↑m (s a)) ≤ ↑m (⋃ (i : ℕ), s i)
refine' iSup_le fun n => _
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
this : ∑ i in Finset.range n, ↑m (univ ∩ s i) = ↑m (univ ∩ ⋃ (i : ℕ) (_ : i < n), s i)
⊢ ∑ a in Finset.range n, ↑m (s a) ≤ ↑m (⋃ (i : ℕ), s i)
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
⊢ ∑ a in Finset.range n, ↑m (s a) ≤ ↑m (⋃ (i : ℕ), s i)
have := @isCaratheodory_sum _ m _ h hd univ n
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
this : ∑ x in Finset.range n, ↑m (s x) = ↑m (⋃ (i : ℕ) (_ : i < n), s i)
⊢ ∑ a in Finset.range n, ↑m (s a) ≤ ↑m (⋃ (i : ℕ), s i)
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
this : ∑ i in Finset.range n, ↑m (univ ∩ s i) = ↑m (univ ∩ ⋃ (i : ℕ) (_ : i < n), s i)
⊢ ∑ a in Finset.range n, ↑m (s a) ≤ ↑m (⋃ (i : ℕ), s i)
simp at this
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
this : ∑ x in Finset.range n, ↑m (s x) = ↑m (⋃ (i : ℕ) (_ : i < n), s i)
⊢ ↑m (⋃ (i : ℕ) (_ : i < n), s i) ≤ ↑m (⋃ (i : ℕ), s i)
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
this : ∑ x in Finset.range n, ↑m (s x) = ↑m (⋃ (i : ℕ) (_ : i < n), s i)
⊢ ∑ a in Finset.range n, ↑m (s a) ≤ ↑m (⋃ (i : ℕ), s i)
simp [this]
no goals
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
n : ℕ
this : ∑ x in Finset.range n, ↑m (s x) = ↑m (⋃ (i : ℕ) (_ : i < n), s i)
⊢ ↑m (⋃ (i : ℕ) (_ : i < n), s i) ≤ ↑m (⋃ (i : ℕ), s i)
exact m.mono (iUnion₂_subset fun i _ => subset_iUnion _ i)