mem_measureSupport — Mathlib

English

If (nhds x).HasBasis p s, then x ∈ μ.support iff ∀ i, p(i) → 0 < μ(s(i)).

Русский

Если (nhds x).HasBasis p s, то x ∈ μ.support тогда и только тогда, когда ∀ i, p(i) → 0 < μ(s(i)).

LaTeX

$$$\\\\forall ι \\ p:\\\\ ι \\to Prop, s:\\\\ι \\to Set X,\t (nhds x).HasBasis p s \\\\Rightarrow x \\in μ.support \\\\Leftrightarrow \\\\forall i, p(i) \\Rightarrow 0 < μ(s(i))$$$

Lean4

theorem _root_.Filter.HasBasis.mem_measureSupport {ι : Sort*} {p : ι → Prop} {s : ι → Set X} {x : X}
    (hl : (𝓝 x).HasBasis p s) : x ∈ μ.support ↔ ∀ (i : ι), p i → 0 < μ (s i) :=
  hl.frequently_smallSets pos_mono

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