mk_coe — Mathlib

English

If you build a StarAlgHom from a function f via a full maker, extensional equality implies the constructed object equals f.

Русский

Если построить StarAlgHom из функции f через конструктор, экстенсивность равенств говорит о равенстве построенного объекта и f.

LaTeX

$$$\text{mk_coe}(f,h_1,\dots, h_6) = f$$$

Lean4

@[simp]
theorem mk_coe (f : A →⋆ₐ[R] B) (h₁ h₂ h₃ h₄ h₅ h₆) : (⟨⟨⟨⟨⟨f, h₁⟩, h₂⟩, h₃, h₄⟩, h₅⟩, h₆⟩ : A →⋆ₐ[R] B) = f :=
  by
  ext
  rfl

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