toFun' — Mathlib

English

The coercion of an open partial homeomorphism to a function is given by its toFun'.

Русский

Родовая карта отображения открытой частичной гомеоморфизмы задается ее toFun'.

LaTeX

$$$toFun' : OpenPartialHomeomorph X Y \to X \to Y$ defined by $e \mapsto e.toFun$.$$

Lean4

/-- Coercion of an open partial homeomorphisms to a function. We don't use `e.toFun` because it is
actually `e.toPartialEquiv.toFun`, so `simp` will apply lemmas about `toPartialEquiv`.
While we may want to switch to this behavior later, doing it mid-port will break a lot of proofs. -/
@[coe]
def toFun' : X → Y :=
  e.toFun

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