ofFunction_le — Mathlib

English

The maximal outer measure bounded by m is the supremum of all outer measures μ with μ(s) ≤ m(s) for all s.

Русский

Максимальная внешняя мера, ограниченная по m, равна супремусу всех внешних мер μ с условием μ(s) ≤ m(s) для всех s.

LaTeX

$$$\\operatorname{ofFunction} m m\\_empty = sSup \\{\\mu \\mid \\forall s, \\mu(s) ≤ m(s)\\}.$$$

Lean4

theorem ofFunction_le (s : Set α) : OuterMeasure.ofFunction m m_empty s ≤ m s :=
  let f : ℕ → Set α := fun i => Nat.casesOn i s fun _ => ∅
  iInf_le_of_le f <|
    iInf_le_of_le (subset_iUnion f 0) <|
      le_of_eq <|
        tsum_eq_single 0 <| by
          rintro (_ | i)
          · simp
          · simp [f, m_empty]

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