cdf_eq_iff

Mathlib.Probability.CDF

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.cdf_eq_iff

← MathLib Explorer

English

CDFs coincide if and only if the measures are equal.

Русский

Если функции распределения совпадают, то меры равны, и наоборот.

LaTeX

$$$ cdf(\mu) = cdf(\nu) \;\Leftrightarrow\; \mu = \nu $$$

Lean4

@[simp]
theorem cdf_eq_iff (μ ν : Measure ℝ) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] : cdf μ = cdf ν ↔ μ = ν :=
  ⟨eq_of_cdf μ ν, fun h ↦ by rw [h]⟩

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

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

Разделы

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

Аффилиация

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