coe_mk' — Mathlib

English

The coercion of mk from a homeomorphism to a continuous multiplicative equivalence is the underlying function.

Русский

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

LaTeX

$$$\operatorname{toFun}(\mathrm{mk} f hf1 hf2) = f$$$

Lean4

@[simp]
theorem coe_mk' (f : M ≃ₜ N) (h : ∀ x y, f (x * y) = f x * f y) : ⇑(mk' f h) = f :=
  rfl

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