one_le_prob_iff

Mathlib.MeasureTheory.Measure.Typeclasses.Probability

URI: https://scilib.ai/kg/mathlib#MeasureTheory.one_le_prob_iff

← MathLib Explorer

English

1 ≤ μ s if and only if μ s = 1, for IsZeroOrProbabilityMeasure μ (simp version).

Русский

1 ≤ μ(s) эквивалентно μ(s) = 1, для μ с нулевой или вероятностной мерой (упрощённо).

LaTeX

$$1 ≤ μ s ↔ μ s = 1$$

Lean4

@[simp]
theorem one_le_prob_iff {μ : Measure α} [IsZeroOrProbabilityMeasure μ] : 1 ≤ μ s ↔ μ s = 1 :=
  ⟨fun h => le_antisymm prob_le_one h, fun h => h ▸ le_refl _⟩

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

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

Разделы

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

Аффилиация

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