mk_coe — Mathlib

English

The canonical function part of the structure built from a bijection f: M ≃ N is exactly f.

Русский

Обозначение функции, получаемое из биекции f: M ≃ N, совпадает с самой f.

LaTeX

$$$(f : M \\simeq N)\\ (hf : \\forall x,y, f(xy)=f(x)f(y)) : (\\mathrm{mk} f hf : M \\to N) = f$$$

Lean4

@[to_additive (attr := simp)]
theorem mk_coe (e : M ≃* N) (e' h₁ h₂ h₃) : (⟨⟨e, e', h₁, h₂⟩, h₃⟩ : M ≃* N) = e :=
  ext fun _ => rfl

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