coe_toEquiv — Mathlib

English

For any e ∈ AddConstEquiv G H a b, the underlying function of e.toEquiv is equal to e; i.e., the coe toEquiv matches the map itself.

Русский

Для любого e ∈ AddConstEquiv G H a b функция, лежащая в основе e.toEquiv, равна e; то есть отображение через toEquiv совпадает с самой функцией e.

LaTeX

$$$ \operatorname{toFun}(e^{\mathrm{toEquiv}}) = e $$$

Lean4

@[simp]
theorem coe_toEquiv (e : G ≃+c[a, b] H) : ⇑e.toEquiv = e :=
  rfl

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