coe_ofClosureMEqTopLeft — Mathlib

English

Given f : M → N and hs : closure s = ⊤, the map ofClosureMEqTopLeft f hs h1 hmul extends f and equals f as a function.

Русский

С учетом hs, отображение ofClosureMEqTopLeft f hs h1 hmul расширяет f и равно f как функция.

LaTeX

$$$\\text{coe}(\\text{ofClosureMEqTopLeft } f) = f$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_ofClosureMEqTopLeft (f : M → N) (hs : closure s = ⊤) (h1 hmul) : ⇑(ofClosureMEqTopLeft f hs h1 hmul) = f :=
  rfl

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