coe_mk_mk — Mathlib · SciLib

English

Another formulation of the same underlying-map equality for a different presentation of mk.

Русский

Другая формулировка того же равенства опорной карты, для иного представления mk.

LaTeX

$$$\forall f\; h_1\; h_2\; h_3,\; (\mathrm{coe} (\mathrm{mk} f\, h_1\, h_2)) = f$$$

Lean4

theorem coe_mk_mk (f : I → X) (h₁) (h₂ : f 0 = x) (h₃ : f 1 = y) : ⇑(mk ⟨f, h₁⟩ h₂ h₃ : Path x y) = f :=
  rfl

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