coe_mk — Mathlib

English

When constructing a coalgebra equivalence from data f and coherence data h, the resulting map’s underlying function is exactly f.

Русский

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

LaTeX

$$$ (\\langle \\langle \\langle \\langle f, h \\rangle, h_0 \\rangle, h_1, h_2 \\rangle, h_3, h_4, h_5 \\rangle : A \\simeq_{\\ell_c[R]} B) = f$$$

Lean4

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

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