apply_coe_symm_apply — Mathlib

English

For any F and x, e ((e : α ≃ β).symm x) = x; i.e., the same general relation as in the basic case.

Русский

Для любого F и x: e((e:α≃β).symm x) = x; та же общая равенство, что и в базовом случае.

LaTeX

$$$e \\big((e:\\alpha \\simeq \\beta).\\mathrm{symm}\\ x\\big)=x$$$

Lean4

@[simp]
theorem _root_.EquivLike.apply_coe_symm_apply {F} [EquivLike F α β] (e : F) (x : β) : e ((e : α ≃ β).symm x) = x :=
  (e : α ≃ β).apply_symm_apply x

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