nonempty

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

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

← MathLib Explorer

English

There exists at least one element in Ω.

Русский

Существует по меньшей мере один элемент в Ω.

LaTeX

$$\\exists x: Ω, True$$

Lean4

theorem nonempty (μ : ProbabilityMeasure Ω) : Nonempty Ω :=
  by
  by_contra maybe_empty
  have zero : (μ : Measure Ω) univ = 0 := by rw [univ_eq_empty_iff.mpr (not_nonempty_iff.mp maybe_empty), measure_empty]
  rw [measure_univ] at zero
  exact zero_ne_one zero.symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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