apprSeq_apply_le_one — Mathlib

English

If μ, μ′ are Haar-like left-invariant measures, then μ′(s) = haarScalarFactor μ′ μ · μ(s) whenever neither μ(s) nor μ′(s) is the top element.

Русский

Если μ и μ′ — лево-инвариантные меры типа Хаара, то μ′(s) =haarScalarFactor μ′ μ · μ(s) при условии, что ни μ(s), ни μ′(s) не равны верхнему элементу.

LaTeX

$$$\\forall G \\; [LocallyCompactSpace G] \\; (μ' : \\mathrm{Measure}(G)) (μ : \\mathrm{Measure}(G)) \\, [\\text{IsHaarMeasure } μ] \\, [\\text{IsFiniteMeasureOnCompacts } μ'] \\, [\\text{IsMulLeftInvariant } μ'] \\, (s : Set G) \\Rightarrow μ s \\neq \\infty \\Rightarrow μ' s \\neq \\infty \\Rightarrow μ' s = haarScalarFactor μ' μ · μ s$$

Lean4

theorem apprSeq_apply_le_one (n : ℕ) (x : X) : hF.apprSeq n x ≤ 1 :=
  (Exists.choose_spec (HasOuterApproxClosed.exAppr F hF)).1 n x

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