support_mono — Mathlib

English

If μ is absolutely continuous with respect to ν (μ ≪ ν), then the support of μ is contained in the support of ν.

Русский

Если мерa μ абсолютно непрерывна по отношению к ν (μ ≪ ν), то опора μ содержится в опоре ν.

LaTeX

$$\\mu \\ll \\nu \\quad\\Rightarrow\\quad \\mathrm{supp}(\\mu) \\subseteq \\mathrm{supp}(\\nu)$$

Lean4

theorem support_mono {μ ν : Measure X} (hμν : μ ≪ ν) : μ.support ⊆ ν.support := fun _ hx ↦
  hx.mp <| .of_forall hμν.pos_mono

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