coe_mk — Mathlib

English

If f is wrapped into a sSupHom via mk with its accompanying data hf, the underlying function of that wrapper is f; i.e., the coercion of mk f hf returns f.

Русский

Если функцию f поместить в структуру sSupHom через конструктор mk с соответствующим доказательством hf, то действующая функция внутри обёртки совпадает с f.

LaTeX

$$$\bigl\langle \mathrm{mk} \, f \, hf \bigr\rangle_{\text{coercion}} = f$$$

Lean4

@[simp, norm_cast]
theorem coe_mk (f : α → β) (hf) : ⇑(mk f hf) = f :=
  rfl

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