extendDomain_eq_embDomain_subtype

English

For f: Subtype P →₀ M, extending the domain is equal to embedding via the subtype embedding; that is, extendDomain f = embDomain (Subtype).subtype f.

Русский

Для f: Subtype P →₀ M, расширение области определения равно вложению через вложение подтипа: extendDomain f = embDomain (Subtype) f.

LaTeX

$$$\\mathrm{extendDomain} f = \\mathrm{embDomain}(.\\mathrm{subtype} P) f$$$

Lean4

theorem extendDomain_eq_embDomain_subtype (f : Subtype P →₀ M) : extendDomain f = embDomain (.subtype _) f :=
  by
  ext a
  by_cases h : P a
  · refine Eq.trans ?_ (embDomain_apply (.subtype P) f (Subtype.mk a h)).symm
    simp [h]
  · rw [embDomain_notin_range, extendDomain_toFun, dif_neg h]
    simp [h]

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