inclusion' — Mathlib

English

Let U be an open subset of a topological space X. The inclusion map i: U → X is a continuous map (the inclusion of the subspace U into X).

Русский

Пусть U — открытое подмножество пространства X. Включение i: U → X является непрерывным отображением (включение подпространства U в X).

LaTeX

$$$i_U: U \\to X\\quad\\text{is continuous}$$$

Lean4

/-- The inclusion map from an open subset to the whole space, as a morphism in `TopCat`.
-/
@[simps! -fullyApplied]
def inclusion' {X : TopCat.{u}} (U : Opens X) : (toTopCat X).obj U ⟶ X :=
  TopCat.ofHom
    { toFun := _
      continuous_toFun := continuous_subtype_val }

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