count_apply_eq_top — Mathlib

English

For a measurable singleton, count s = ∞ iff s is infinite, under appropriate singleton measurability assumptions.

Русский

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

LaTeX

$$$count\;s = \infty \iff s \text{ is infinite}$$$

Lean4

@[simp]
theorem count_apply_eq_top [MeasurableSingletonClass α] : count s = ∞ ↔ s.Infinite :=
  by
  by_cases hs : s.Finite
  · exact count_apply_eq_top' hs.measurableSet
  · change s.Infinite at hs
    simp [hs, count_apply_infinite]

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