mk_coe — Mathlib

English

A constructor with components equals the original morphism when assembled.

Русский

Конструктор из составляющих возвращает исходный морфизм, когда собрать их в одну структуру.

LaTeX

$$$\\mathrm{mk}(f,h_0,h_1,h_2,h_3,h_4,h_5) = f$$$

Lean4

@[simp]
theorem mk_coe {f : A →ₐc[R] B} (h₀ h₁ h₂ h₃ h₄ h₅) : (⟨⟨⟨⟨f, h₀⟩, h₁⟩, h₂, h₃⟩, h₄, h₅⟩ : A →ₐc[R] B) = f :=
  rfl

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