ofTop_symm_apply_coe — Mathlib

English

When an equality holds by reflexivity, the corresponding affine isometry equality reduces to identity.

Русский

Когда равенство следует из рефлексивности, соответствующее равенство аффинной эквивалентности сводится к тождеству.

LaTeX

$$$\mathrm{ofEq}(s_1,s_1,rfl) = \mathrm{refl}$$$

Lean4

@[simp]
theorem ofTop_symm_apply_coe (h : s₁ = ⊤) (x : P) : (ofTop s₁ h).symm x = x :=
  rfl

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