no goals
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
x✝ : ∀ (i : ℕ), i < 0 → IsCaratheodory m (s i)
⊢ IsCaratheodory m (⋃ (i : ℕ) (_ : i < 0), s i)
simp [Nat.not_lt_zero]
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
n : ℕ
h : ∀ (i : ℕ), i < n + 1 → IsCaratheodory m (s i)
⊢ IsCaratheodory m ((⋃ (k : ℕ) (_ : k < n), s k) ∪ s n)
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
n : ℕ
h : ∀ (i : ℕ), i < n + 1 → IsCaratheodory m (s i)
⊢ IsCaratheodory m (⋃ (i : ℕ) (_ : i < n + 1), s i)
rw [biUnion_lt_succ]
no goals
α : Type u
m : OuterMeasure α
s✝ s₁ s₂ : Set α
s : ℕ → Set α
n : ℕ
h : ∀ (i : ℕ), i < n + 1 → IsCaratheodory m (s i)
⊢ IsCaratheodory m ((⋃ (k : ℕ) (_ : k < n), s k) ∪ s n)
exact isCaratheodory_union m
        (isCaratheodory_iUnion_lt fun i hi => h i <| lt_of_lt_of_le hi <| Nat.le_succ _)
        (h n (le_refl (n + 1)))