coe_mk — Mathlib

English

Constructing a StarAlgHom from a plain function with proofs yields a function that equals the original function under coercion.

Русский

Построение StarAlgHom из простой функции с необходимыми доказательствами даёт отображение, чья когерентная функция совпадает с исходной функцией под приводом.

LaTeX

$$$\text{coerce}(⟨f,\dots⟩)=f$$$

Lean4

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

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