isOpenPosMeasure_of_mulLeftInvariant_of_innerRegular

English

A nonzero left-invariant inner regular measure assigns positive mass to any nonempty open set.

Русский

Непрерывная левая инвариантная внутренняя регулярная мера равна: μ(U) > 0 для любого ненулевого открытого множества U.

LaTeX

$$$\forall U\, (\text{IsOpen}(U) \land U \neq \emptyset) \Rightarrow \mu(U) > 0$$$

Lean4

/-- A nonzero left-invariant inner regular measure gives positive mass to any open set. -/
@[to_additive /-- A nonzero left-invariant inner regular measure gives positive mass to any open set. -/
    ]
instance (priority := 80) isOpenPosMeasure_of_mulLeftInvariant_of_innerRegular [InnerRegular μ] [NeZero μ] :
    IsOpenPosMeasure μ :=
  let ⟨K, hK, h2K⟩ := InnerRegular.exists_isCompact_not_null.mpr (NeZero.ne μ)
  isOpenPosMeasure_of_mulLeftInvariant_of_compact K hK h2K

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