mk_coe — Mathlib

English

Coercion of an OpenPartialHomeomorph to a function is the same as the underlying function; i.e., the OpenPartialHomeomorph coerces to its toFun component.

Русский

Коэрцирование открыто‑частичного гомеоморфизма к функции совпадает с его основным компонентом toFun.

LaTeX

$$$ (e : OpenPartialHomeomorph X Y).toPartialEquiv : X \to Y = e $$$

Lean4

@[simp, mfld_simps]
theorem mk_coe (e : PartialEquiv X Y) (a b c d) : (OpenPartialHomeomorph.mk e a b c d : X → Y) = e :=
  rfl

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