coe_coe — Mathlib

English

The coe from EquivLike to Equiv and then back preserves the original function: toFunLike.coe (toEquiv e) = toFunLike e.

Русский

Коэффициентная функция из EquivLike в Equiv и обратно сохраняет исходную функцию: toFunLike.coe (toEquiv e) = toFunLike e.

LaTeX

$$$\\operatorname{toFunLike}(\\operatorname{toEquiv}(e)) = \\operatorname{toFunLike}(e).$$$

Lean4

@[simp, norm_cast]
theorem _root_.EquivLike.coe_coe {F} [EquivLike F α β] (e : F) : ((e : α ≃ β) : α → β) = e :=
  rfl

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