toFun' — Mathlib

English

The coercion from ModelWithCorners to functions is defined; it maps a model instance to its evaluation function.

Русский

Приведение модели с углами к функциям определено; оно отображает экземпляр модели на его функционал оценки.

LaTeX

$$$toFun' : ModelWithCorners 𝕜 E H \\to H \\to E$$$

Lean4

/-- Coercion of a model with corners 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' (e : ModelWithCorners 𝕜 E H) : H → E :=
  e.toFun

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