instInhabited

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

URI: https://scilib.ai/kg/mathlib#MeasureTheory.ProbabilityMeasure.instInhabited

English

If E is clopen, the sequence of measures μ_s(i,E) converges to μ(E).

Русский

Если E открыто и замкнуто одновременно, тогда μ_s(i,E) сходится к μ(E).

LaTeX

$$$\forall E\; (\text{IsClopen}(E)) \Rightarrow \text{Tendsto}(i\mapsto μ_s(i,E)) L (\mathcal{N}(μ(E)))$$$

Lean4

instance [Inhabited Ω] : Inhabited (ProbabilityMeasure Ω) :=
  ⟨⟨Measure.dirac default, Measure.dirac.isProbabilityMeasure⟩⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru