mk_coe_symm — Mathlib

English

The OpenPartialHomeomorph constructed from a partial equivalence has as its function the given map; i.e., its representation as a function equals the original partial equivalence.

Русский

Частично‑гомеоморфизм, построенный из частичного эквивалента, имеет в качестве функции заданное отображение; тождество представления как функции и исходного частичного эквивалента.

LaTeX

$$$ (\mathrm{OpenPartialHomeomorph.mk} e a b c d : X \to Y) = e.$$$

Lean4

@[simp, mfld_simps]
theorem mk_coe_symm (e : PartialEquiv X Y) (a b c d) : ((OpenPartialHomeomorph.mk e a b c d).symm : Y → X) = e.symm :=
  rfl

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