openPartialHomeomorphSubtypeCoe_coe

English

The inclusion map from the subtype s.openPartialHomeomorphSubtypeCoe hs to X is the same as the canonical coercion, i.e., the function is the inclusion map.

Русский

Вложение из подтипа s.openPartialHomeomorphSubtypeCoe hs в X совпадает с канонической привязкой к типу X, то есть это просто включение.

LaTeX

$$$ (s.openPartialHomeomorphSubtypeCoe hs : s \to X) = \iota_s $ (inclusion to X) $$

Lean4

@[simp, mfld_simps]
theorem openPartialHomeomorphSubtypeCoe_coe : (s.openPartialHomeomorphSubtypeCoe hs : s → X) = (↑) :=
  rfl

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