toFun' — Mathlib

English

A pretrivialization e can be viewed as a function from Z to B × F, given by its toFun'.

Русский

Предтривиализация e может рассматриваться как функция от Z в B × F, заданная через toFun'.

LaTeX

$$$toFun' = e.toFun$$$

Lean4

/-- Coercion of a pretrivialization to a function. We don't use `e.toFun` in the `CoeFun` instance
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' : Z → (B × F) :=
  e.toFun

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