inducedOuterMeasure_eq' — Mathlib

English

An alternative formulation of the iInf expression of the induced outer measure as an infimum over all t with Pt containing s.

Русский

Альтернатива формулировки через infimum по всем t с Pt, содержащим s.

LaTeX

$$$\\mathrm{inducedOuterMeasure}\\ m P0 m0 s = \\inf_{t: Set\\alpha}\\; ht\\; (s \\subseteq t)\\; m t ht$$$

Lean4

theorem inducedOuterMeasure_eq' {s : Set α} (hs : P s) : inducedOuterMeasure m P0 m0 s = m s hs :=
  (inducedOuterMeasure_eq_extend' PU msU m_mono hs).trans <| extend_eq _ _

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