levyProkhorovEDist_le_max_measure_univ

English

For measures μ, ν on Ω, levyProkhorovEDist μ ν ≤ max(μ(Ω), ν(Ω)).

Русский

Для мер μ, ν на Ω выполняется неравенство: levyProkhorovEDist μ ν ≤ max(μ(Ω), ν(Ω)).

LaTeX

$$$$ \ levyProkhorovEDist(\mu,\nu) \le \max(\mu(\Omega),\nu(\Omega)). $$$$

Lean4

theorem levyProkhorovEDist_le_max_measure_univ (μ ν : Measure Ω) : levyProkhorovEDist μ ν ≤ max (μ univ) (ν univ) := by
  refine sInf_le fun B _ ↦ ⟨?_, ?_⟩ <;> apply le_add_left <;> simp [measure_mono]

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