boundedBy_eq_ofFunction — Mathlib

English

If m is a set function with m(∅) = 0, then for every s, boundedBy m s equals OuterMeasure.ofFunction m m_empty s.

Русский

Если m — функция на множествах и m(∅) = 0, то для любого s выполняется boundedBy m s = OuterMeasure.ofFunction m m_empty s.

LaTeX

$$$\\text{boundedBy } m\\, s = \\mathrm{OuterMeasure.ofFunction } m\\, m_{\\emptyset}\\, s$$$

Lean4

theorem boundedBy_eq_ofFunction (m_empty : m ∅ = 0) (s : Set α) : boundedBy m s = OuterMeasure.ofFunction m m_empty s :=
  by
  have : (fun s : Set α => ⨆ _ : s.Nonempty, m s) = m := by
    ext1 t
    rcases t.eq_empty_or_nonempty with h | h <;> simp [h, Set.not_nonempty_empty, m_empty]
  simp [boundedBy, this]

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