isCaratheodory_partialSups — Mathlib

English

For a family s: ι → Set α, if every s i is Carathéodory, then for each i, partialSups s i is Carathéodory.

Русский

Для семейства s: ι → Set α, если для каждого i выполняется IsCaratheodory (s i), то IsCaratheodory (partialSups s i).

LaTeX

$$∀ i, m.IsCaratheodory (partialSups s i)$$

Lean4

theorem isCaratheodory_partialSups {ι : Type*} [Preorder ι] [LocallyFiniteOrderBot ι] {s : ι → Set α}
    (h : ∀ i, m.IsCaratheodory (s i)) (i : ι) : m.IsCaratheodory (partialSups s i) := by
  simpa only [partialSups_apply, Finset.sup'_eq_sup, Finset.sup_set_eq_biUnion, ← Finset.mem_coe, Finset.coe_Iic] using
    .biUnion_of_finite (finite_Iic _) (fun j _ ↦ h j)

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