English
Under the standard setup, mkMetric m s ≤ liminf (∑' i, m (diam (t n i))) l for appropriate families t.
Русский
В общих условиях mkMetric m s ≤ liminf (∑' i, m (diam (t n i))) l для соответствующих семейств t.
LaTeX
$$$ mkMetric m s \le \liminf_{n} \sum_i m(\operatorname{diam}(t_n i)) $$$
Lean4
/-- To bound the Hausdorff measure (or, more generally, for a measure defined using
`MeasureTheory.Measure.mkMetric`) of a set, one may use coverings with maximum diameter tending to
`0`, indexed by any sequence of finite types. -/
theorem mkMetric_le_liminf_sum {β : Type*} {ι : β → Type*} [hι : ∀ n, Fintype (ι n)] (s : Set X) {l : Filter β}
(r : β → ℝ≥0∞) (hr : Tendsto r l (𝓝 0)) (t : ∀ n : β, ι n → Set X) (ht : ∀ᶠ n in l, ∀ i, diam (t n i) ≤ r n)
(hst : ∀ᶠ n in l, s ⊆ ⋃ i, t n i) (m : ℝ≥0∞ → ℝ≥0∞) : mkMetric m s ≤ liminf (fun n => ∑ i, m (diam (t n i))) l := by
simpa only [tsum_fintype] using mkMetric_le_liminf_tsum s r hr t ht hst m
