uniformOn_eq_zero' — Mathlib

English

For measurable s, uniformOn s = 0 iff s is infinite or empty.

Русский

Для измеримого множества s: uniformOn s = 0 тогда и только тогда, когда s бесконечно или пусто.

LaTeX

$$$uniformOn\;s = 0 \Leftrightarrow s\text{ бесконечно или } s = \varnothing$$$

Lean4

/-- See `uniformOn_eq_zero` for a version assuming `MeasurableSingletonClass Ω` instead of
`MeasurableSet s`. -/
@[simp]
theorem uniformOn_eq_zero' (hs : MeasurableSet s) : uniformOn s = 0 ↔ s.Infinite ∨ s = ∅ := by simp [uniformOn, hs]

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