hausdorffMeasure_le_liminf_sum — Mathlib

English

If d1 < d2, then for every set s either μH[d2] s = 0 or μH[d1] s = ∞.

Русский

Если d1 < d2, то для любого множества s либо μH[d2] s = 0, либо μH[d1] s = ∞.

LaTeX

$$$ μH[d2] s = 0 \; \lor \; μH[d1] s = ∞ $$$

Lean4

/-- To bound the Hausdorff measure of a set, one may use coverings with maximum diameter tending
to `0`, indexed by any sequence of finite types. -/
theorem hausdorffMeasure_le_liminf_sum {β : Type*} {ι : β → Type*} [∀ n, Fintype (ι n)] (d : ℝ) (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) :
    μH[d] s ≤ liminf (fun n => ∑ i, diam (t n i) ^ d) l :=
  mkMetric_le_liminf_sum s r hr t ht hst _

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