toFun' — Mathlib

English

Another variant of extensionality for trivializations with matching data.

Русский

Еще одно повторение экстенсиональности для тривиализаций.

LaTeX

$$$e.toOpenPartialHomeomorph = e'.toOpenPartialHomeomorph\land\; e.baseSet = e'.baseSet\Rightarrow e = e'$$$

Lean4

/-- Coercion of a trivialization 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

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