outerMeasure_of_isOpen — Mathlib

English

Another form of equality on opens: the outer measure equals inner content for open U.

Русский

Еще одна форма равенства на открытых множествах: внешняя мера равна внутренному содержимому для открытого U.

LaTeX

$$$\mu.outerMeasure(U) = μ.innerContent(U)$$$

Lean4

theorem outerMeasure_of_isOpen (U : Set G) (hU : IsOpen U) : μ.outerMeasure U = μ.innerContent ⟨U, hU⟩ :=
  μ.outerMeasure_opens ⟨U, hU⟩

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