instTietzeExtensionClosedBall — Mathlib

English

Let E be a finite-dimensional normed space over a field with RCLike structure. For any y in E and any radius r > 0, the closed ball around y of radius r admits the Tietze extension property: every continuous function f from the closed ball to the real numbers extends to a continuous function on the whole space E.

Русский

Пусть E — нормированное пространство над полем с конструкцией RCLike и пусть y ∈ E, r > 0. Замкнутый шар окрестности y радиуса r обладает свойством расширения Титце: любая непрерывная функция f: замкнутый шар → ℝ может быть продолжена до непрерывной функции на всём пространстве E.

LaTeX

$$$$ \forall f \in C\bigl(\overline{B}(y,r), \mathbb{R}\bigr),\ \exists F \in C(E, \mathbb{R}) \bigl( F|_{\overline{B}(y,r)} = f \bigr). $$$$

Lean4

theorem instTietzeExtensionClosedBall (𝕜 : Type v) [RCLike 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    [FiniteDimensional 𝕜 E] (y : E) {r : ℝ} (hr : 0 < r) : TietzeExtension.{u, w} (Metric.closedBall y r) :=
  .of_homeo <| by
    change (Metric.closedBall y r) ≃ₜ (Metric.closedBall (0 : E) 1)
    symm
    apply (DilationEquiv.smulTorsor y (k := (r : 𝕜)) <| by exact_mod_cast hr.ne').toHomeomorph.sets
    ext x
    simp only [mem_closedBall, dist_zero_right, DilationEquiv.coe_toHomeomorph, Set.mem_preimage,
      DilationEquiv.smulTorsor_apply, vadd_eq_add, dist_add_self_left, norm_smul, RCLike.norm_ofReal,
      abs_of_nonneg hr.le]
    exact (mul_le_iff_le_one_right hr).symm

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