instMonoDiskBoundaryInclusion — Mathlib

English

The inclusion ∂D^n → D^n is a monomorphism in the category of topological spaces, i.e., injective.

Русский

Включение ∂D^n → D^n является монообразным в категории топологических пространств, т.е. инъективно.

LaTeX

$$$\\text{Mono}(\\iota_{\\partial D^n \\to D^n}).$$$

Lean4

instance {n : ℕ} : Mono (diskBoundaryInclusion n) :=
  mono_iff_injective _ |>.mpr <| by
    intro ⟨x, hx⟩ ⟨y, hy⟩ h
    obtain rfl : x = y := by simpa [diskBoundaryInclusion, disk] using h
    congr

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