diskBoundaryInclusion — Mathlib

English

The inclusion map ∂D^n → D^n is a natural topological embedding.

Русский

Включение ∂D^n ↪ D^n является естественным вложением топологических пространств.

LaTeX

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

Lean4

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

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