isOpenPosMeasure_of_mulLeftInvariant_of_regular

English

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

Русский

Непрерывная левая инвариантная мера с μ ≠ 0 присваивает положительную массу каждому ненулевому открытому множеству.

LaTeX

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

Lean4

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

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