coe_inclusion' — Mathlib

English

The inclusion map i_U : U → X is exactly the standard Subtype.val map, i.e., the underlying function is the inclusion of the subtype into X.

Русский

Включение i_U : U → X является обычной отображающей функцией Subtype.val: подпростество U включается в X через отображение-«значение» его элементов.

LaTeX

$$$(inclusion_U : U \\to X) = \\mathrm{Subtype.val}$$$

Lean4

@[simp]
theorem coe_inclusion' {X : TopCat} {U : Opens X} : (inclusion' U : U → X) = Subtype.val :=
  rfl

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