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 α
⊢ ∑ i in Finset.range 0, ↑m (t ∩ s i) = ↑m (t ∩ ⋃ (i : ℕ) (_ : i < 0), s i)
simp [Nat.not_lt_zero, m.empty]
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
n : ℕ
⊢ (s n ∩ ⋃ (k : ℕ) (_ : k < n), s k) ⊆ ∅
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
n : ℕ
⊢ ∑ i in Finset.range (Nat.succ n), ↑m (t ∩ s i) = ↑m (t ∩ ⋃ (i : ℕ) (_ : i < Nat.succ n), s i)
rw [biUnion_lt_succ, Finset.sum_range_succ, Set.union_comm, isCaratheodory_sum h hd,
  m.measure_inter_union _ (h n), add_comm]
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
n : ℕ
a : α
⊢ (a ∈ s n ∩ ⋃ (k : ℕ) (_ : k < n), s k) → a ∈ ∅
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
h : ∀ (i : ℕ), IsCaratheodory m (s i)
hd : Pairwise (Disjoint on s)
t : Set α
n : ℕ
⊢ (s n ∩ ⋃ (k : ℕ) (_ : k < n), s k) ⊆ ∅
intro a
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 α
n : ℕ
a : α
⊢ (a ∈ s n ∩ ⋃ (k : ℕ) (_ : k < n), s k) → a ∈ ∅
simpa using fun (h₁ : a ∈ s n) i (hi : i < n) h₂ => (hd (ne_of_gt hi)).le_bot ⟨h₁, h₂⟩