sSup_apply — Mathlib

English

The value of the supremum outer measure sSup over a set ms, at a set s, is the supremum of the values m(s) over m ∈ ms.

Русский

Значение верхней меры-объединения sSup по множеству внешних мер ms в точке s равно наибольшему значению m(s) среди m ∈ ms.

LaTeX

$$$(\mathrm{sSup}\ ms)(s) = \sup_{m \in ms} (m(s)).$$$

Lean4

@[simp]
theorem sSup_apply (ms : Set (OuterMeasure α)) (s : Set α) : (sSup ms) s = ⨆ m ∈ ms, (m : OuterMeasure α) s :=
  rfl

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