English
If s is infinite and each x ∈ s has μ({x}) ≥ ε > 0, then μ(s) = ∞.
Русский
Если s бесконечно, и каждый x ∈ s удовлетворяет μ({x}) ≥ ε > 0, то μ(s) = ∞.
LaTeX
$$If s is infinite and ∃ ε > 0 with ∀ x ∈ s, ε ≤ μ({x}) then μ(s) = ∞$$
Lean4
/-- If all elements of an infinite set have measure uniformly separated from zero,
then the set has infinite measure. -/
theorem _root_.Set.Infinite.meas_eq_top [MeasurableSingletonClass α] {s : Set α} (hs : s.Infinite)
(h' : ∃ ε, ε ≠ 0 ∧ ∀ x ∈ s, ε ≤ μ { x }) : μ s = ∞ :=
top_unique <|
let ⟨ε, hne, hε⟩ := h';
have := hs.to_subtype
calc
∞ = ∑' _ : s, ε := (ENNReal.tsum_const_eq_top_of_ne_zero hne).symm
_ ≤ ∑' x : s, μ { x.1 } := (ENNReal.tsum_le_tsum fun x ↦ hε x x.2)
_ ≤ μ (⋃ x : s, { x.1 }) :=
(tsum_meas_le_meas_iUnion_of_disjoint _ (fun _ ↦ MeasurableSet.singleton _) fun x y hne ↦ by
simpa [Subtype.val_inj])
_ = μ s := by simp
