coe_symm_mk — Mathlib

English

The inverse map of the constructed partial equivalence equals the given g.

Русский

Обратная карта сконструированного частичного эквивалента равна заданной функции g.

LaTeX

$$$((\mathrm{PartialEquiv.mk}\ f\ g\ s\ t\ ml\ mr\ il\ ir).\mathrm{symm} : \beta \to \alpha) = g$$$

Lean4

@[simp, mfld_simps]
theorem coe_symm_mk (f : α → β) (g s t ml mr il ir) : ((PartialEquiv.mk f g s t ml mr il ir).symm : β → α) = g :=
  rfl

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