coe_mk — Mathlib

English

If f is a MulEquiv with continuous toFun and continuous invFun, then the continuous equivalent built from f coincides with f.

Русский

Если f — MulEquiv с непрерывной функцией и непрерывной обратной функцией, то непрерывное соответствие, построенное из f, совпадает с f.

LaTeX

$$$\mathrm{mk}(f\, hf1\, hf2)\;\text{coercion to function} = f$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_mk (f : M ≃* N) (hf1 hf2) : ⇑(mk f hf1 hf2) = f :=
  rfl

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