α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
⊢ ∀ (t : Set α), ↑m (t ∩ ⋃ (i : ℕ), s i) + ↑m (t \ ⋃ (i : ℕ), s i) ≤ ↑m t
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
⊢ IsCaratheodory m (⋃ (i : ℕ), s i)
apply (isCaratheodory_iff_le' m).mpr
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ ↑m (t ∩ ⋃ (i : ℕ), s i) + ↑m (t \ ⋃ (i : ℕ), s i) ≤ ↑m t
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
⊢ ∀ (t : Set α), ↑m (t ∩ ⋃ (i : ℕ), s i) + ↑m (t \ ⋃ (i : ℕ), s i) ≤ ↑m t
intro t
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : ↑m (t ∩ ⋃ (i : ℕ), s i) ≤ ⨆ (n : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < n), s i)
⊢ ↑m (t ∩ ⋃ (i : ℕ), s i) + ↑m (t \ ⋃ (i : ℕ), s i) ≤ ↑m t
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ ↑m (t ∩ ⋃ (i : ℕ), s i) + ↑m (t \ ⋃ (i : ℕ), s i) ≤ ↑m t
have hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i < n, s i) := by
  convert m.iUnion fun i => t ∩ s i using 1
  . simp [inter_iUnion]
  . simp [ENNReal.tsum_eq_iSup_nat, isCaratheodory_sum m h hd]
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : ↑m (t ∩ ⋃ (i : ℕ), s i) ≤ ⨆ (n : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < n), s i)
⊢ (⨆ (n : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < n), s i)) + ↑m (t \ ⋃ (i : ℕ), s i) ≤ ↑m t
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : ↑m (t ∩ ⋃ (i : ℕ), s i) ≤ ⨆ (n : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < n), s i)
⊢ ↑m (t ∩ ⋃ (i : ℕ), s i) + ↑m (t \ ⋃ (i : ℕ), s i) ≤ ↑m t
refine' le_trans (add_le_add_right hp _) _
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : ↑m (t ∩ ⋃ (i : ℕ), s i) ≤ ⨆ (n : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < n), s i)
⊢ (⨆ (b : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < b), s i) + ↑m (t \ ⋃ (i : ℕ), s i)) ≤ ↑m t
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : ↑m (t ∩ ⋃ (i : ℕ), s i) ≤ ⨆ (n : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < n), s i)
⊢ (⨆ (n : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < n), s i)) + ↑m (t \ ⋃ (i : ℕ), s i) ≤ ↑m t
rw [ENNReal.iSup_add]
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : ↑m (t ∩ ⋃ (i : ℕ), s i) ≤ ⨆ (n : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < n), s i)
n : ℕ
⊢ ↑m (t \ ⋃ (i : ℕ), s i) ≤ ↑m (t \ ⋃ (i : ℕ) (_ : i < n), s i)
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : ↑m (t ∩ ⋃ (i : ℕ), s i) ≤ ⨆ (n : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < n), s i)
⊢ (⨆ (b : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < b), s i) + ↑m (t \ ⋃ (i : ℕ), s i)) ≤ ↑m t
refine'
  iSup_le fun n =>
    le_trans (add_le_add_left _ _) (ge_of_eq (isCaratheodory_iUnion_lt m (fun i _ => h i) _))
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : ↑m (t ∩ ⋃ (i : ℕ), s i) ≤ ⨆ (n : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < n), s i)
n : ℕ
⊢ (⋃ (i : ℕ) (_ : i < n), s i) ⊆ ⋃ (i : ℕ), s i
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : ↑m (t ∩ ⋃ (i : ℕ), s i) ≤ ⨆ (n : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < n), s i)
n : ℕ
⊢ ↑m (t \ ⋃ (i : ℕ), s i) ≤ ↑m (t \ ⋃ (i : ℕ) (_ : i < n), s i)
refine' m.mono (diff_subset_diff_right _)
no goals
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : ↑m (t ∩ ⋃ (i : ℕ), s i) ≤ ⨆ (n : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < n), s i)
n : ℕ
⊢ (⋃ (i : ℕ) (_ : i < n), s i) ⊆ ⋃ (i : ℕ), s i
exact iUnion₂_subset fun i _ => subset_iUnion _ i
case h.e'_3
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ ↑m (t ∩ ⋃ (i : ℕ), s i) = ↑m (⋃ (i : ℕ), t ∩ s i)

case h.e'_4
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ (⨆ (n : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < n), s i)) = ∑' (i : ℕ), ↑m (t ∩ s i)
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ ↑m (t ∩ ⋃ (i : ℕ), s i) ≤ ⨆ (n : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < n), s i)
convert m.iUnion fun i => t ∩ s i using 1
case h.e'_4
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ (⨆ (n : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < n), s i)) = ∑' (i : ℕ), ↑m (t ∩ s i)
case h.e'_3
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ ↑m (t ∩ ⋃ (i : ℕ), s i) = ↑m (⋃ (i : ℕ), t ∩ s i)

case h.e'_4
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ (⨆ (n : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < n), s i)) = ∑' (i : ℕ), ↑m (t ∩ s i)
. simp [inter_iUnion]
no goals
case h.e'_4
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ (⨆ (n : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < n), s i)) = ∑' (i : ℕ), ↑m (t ∩ s i)
. simp [ENNReal.tsum_eq_iSup_nat, isCaratheodory_sum m h hd]
no goals
case h.e'_3
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ ↑m (t ∩ ⋃ (i : ℕ), s i) = ↑m (⋃ (i : ℕ), t ∩ s i)
simp [inter_iUnion]
no goals
case h.e'_4
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ (⨆ (n : ℕ), ↑m (t ∩ ⋃ (i : ℕ) (_ : i < n), s i)) = ∑' (i : ℕ), ↑m (t ∩ s i)
simp [ENNReal.tsum_eq_iSup_nat, isCaratheodory_sum m h hd]