iSup_apply — Mathlib

English

Let f_i be a family of outer measures on a set X, indexed by i in ι. Then the outer measure given by the pointwise supremum satisfies for every S: (⨆ i, f_i)(S) = ⨆ i, f_i(S).

Русский

Пусть f_i — семейство внешних мер на множества X, индексируемое i из ι. Тогда внешняя мера, заданная как точечная сводка, удовлетворяет для каждого S: (⨆ i, f_i)(S) = ⨆ i, f_i(S).

LaTeX

$$$ (\big\vee_{i} f_i)(S) = \big\vee_{i} f_i(S) $$$

Lean4

@[simp]
theorem iSup_apply {ι} (f : ι → OuterMeasure α) (s : Set α) : (⨆ i : ι, f i) s = ⨆ i, f i s := by
  rw [iSup, sSup_apply, iSup_range]

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