instTietzeExtensionBall — Mathlib

English

There is a Tietze extension on the metric ball around the origin with radius r > 0, via a homeomorphism with the unit ball.

Русский

Существует расширение Титце на метрическом шаре вокруг начала координат радиуса r > 0, через гомоморфизм с единичным шаром.

LaTeX

$$TietzeExtension (Metric.ball 0 r)$$

Lean4

theorem instTietzeExtensionBall {𝕜 : Type v} [RCLike 𝕜] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    [FiniteDimensional 𝕜 E] {r : ℝ} (hr : 0 < r) : TietzeExtension.{u, w} (Metric.ball (0 : E) r) :=
  have : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
  .of_homeo <|
    show (Metric.ball (0 : E) r) ≃ₜ (Metric.ball (0 : E) 1) from
      OpenPartialHomeomorph.unitBallBall (0 : E) r hr |>.toHomeomorphSourceTarget.symm

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