instInnerRegularCompactLTTop — Mathlib

English

If μ is regular, then it is inner regular with respect to compact sets over measurable sets of finite measure, i.e., approximations by compact subsets exist.

Русский

Если μ регулярная, то она внутренняя регулярна по отношению к компактным множестваам на множествах с конечной мерой.

LaTeX

$$$\\text{Regular}(\\mu)\\implies \\text{InnerRegularCompactLTTop}(\\mu).$$$

Lean4

/-- If `μ` is a regular measure, then any measurable set of finite measure can be approximated by a
compact subset. See also `MeasurableSet.exists_isCompact_lt_add` and
`MeasurableSet.exists_lt_isCompact_of_ne_top`. -/
instance (priority := 100) [Regular μ] : InnerRegularCompactLTTop μ :=
  ⟨Regular.innerRegular.measurableSet_of_isOpen (fun _ _ hs hU ↦ hs.diff hU)⟩

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