isCaratheodory_iUnion_lt — Mathlib

English

If for every i < n, s_i is Carathéodory, then the union over i < n is Carathéodory.

Русский

Если для каждого i < n множество s_i карatheodory, то объединение ⋃_{i < n} s_i карatheodory.

LaTeX

$$∀ n, (∀ i < n, m.IsCaratheodory (s i)) → m.IsCaratheodory (⋃ i < n, s i)$$

Lean4

theorem isCaratheodory_iUnion_lt {s : ℕ → Set α} :
    ∀ {n : ℕ}, (∀ i < n, IsCaratheodory m (s i)) → IsCaratheodory m (⋃ i < n, s i)
  | 0, _ => by simp
  | n + 1, h => by
    rw [biUnion_lt_succ]
    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)))

Похожие утверждения