biInf_apply' — Mathlib

English

A variant form of biInf applying to a subset I of indices and nonempty I.

Русский

Вариант биInf, применимый к подкоторке индексов I и непустого I.

LaTeX

$$$\\mathrm{biInf}\\, m\\, s = \\inf_{t: \\mathbb{N} \\to Set\\alpha} \\inf_{x} \\sum' n, \\inf_{i \\in I} m_i (t n)$$$

Lean4

/-- The value of the Infimum of a nonempty family of outer measures on a set is not simply
the minimum value of a measure on that set: it is the infimum sum of measures of countable set of
sets that covers that set, where a different measure can be used for each set in the cover. -/
theorem biInf_apply' {ι} (I : Set ι) (m : ι → OuterMeasure α) {s : Set α} (hs : s.Nonempty) :
    (⨅ i ∈ I, m i) s = ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' n, ⨅ i ∈ I, m i (t n) := by
  simp only [← iInf_subtype'', iInf_apply' _ hs]

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