instInnerRegularOfIsFiniteMeasure

English

If μ is inner regular for finite measure sets with respect to compact sets and μ is finite, then μ is inner regular in the standard sense.

Русский

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

LaTeX

$$$[InnerRegularCompactLTTop μ]\\; [IsFiniteMeasure μ] \\Rightarrow InnerRegular μ$$$

Lean4

instance (priority := 50) [h : InnerRegularCompactLTTop μ] [IsFiniteMeasure μ] : InnerRegular μ :=
  by
  constructor
  convert h.innerRegular with s
  simp [measure_ne_top μ s]

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