ballInclusion — Mathlib

English

The inclusion map 𝔹^n → D^n is the natural inclusion of the interior into the disk.

Русский

Включение 𝔹^n → D^n есть естественное вложение внутренности в диск.

LaTeX

$$$\\iota_{\\mathbb{B}^n \\to D^n} : \\mathbb{B}^n \\hookrightarrow D^n.$$$

Lean4

/-- The inclusion `𝔹 n ⟶ 𝔻 n` of the interior of the `n`-disk. -/
def ballInclusion (n : ℕ) : 𝔹 n ⟶ 𝔻 n :=
  ofHom
    { toFun := fun ⟨p, hp⟩ ↦ ⟨p, Metric.ball_subset_closedBall hp⟩
      continuous_toFun :=
        ⟨fun t ⟨s, ⟨r, hro, hrs⟩, hst⟩ ↦ by
          rw [isOpen_induced_iff, ← hst, ← hrs]
          tauto⟩ }

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