dimH_lt_top — Mathlib

English

Let f: E→F be C¹ on finite-dimensional spaces. If dim_H(t) < dim(F) for t ⊆ E, then the complement of the image f(t) is dense in F.

Русский

Пусть f: E→F гладкая (C¹). Если dim_H(t) < dim(F) для подмножества t ⊆ E, то дополнение изображения f(t) плотно в F.

LaTeX

$$Dense(F \\ f(t))$$

Lean4

/-- The Hausdorff dimension of any set in a finite-dimensional real normed space is finite. -/
theorem dimH_lt_top (s : Set E) : dimH s < ⊤ := by
  calc
    dimH s ≤ dimH (univ : Set E) := dimH_mono (subset_univ s)
    _ = finrank ℝ E := (dimH_univ_eq_finrank E)
    _ < ⊤ := by simp

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