count_apply_eq_top' — Mathlib

English

For a measurable set s, count s = ∞ if and only if s is infinite.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem count_apply_eq_top' (s_mble : MeasurableSet s) : count s = ∞ ↔ s.Infinite :=
  by
  by_cases hs : s.Finite
  · simp [Set.Infinite, hs, count_apply_finite' hs s_mble]
  · change s.Infinite at hs
    simp [hs, count_apply_infinite]

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