mk_symm — Mathlib

English

The symmetry of the constructed model equals the original partial equivalence's symmetry: (ModelWithCorners.mk e a b c d d').symm = e.symm.

Русский

Симметрия построенной модели равна симметрии исходного частичного эквивалента: (ModelWithCorners.mk e a b c d d').symm = e.symm.

LaTeX

$$$ (\\mathrm{ModelWithCorners.mk}\\, e\\ a\\ b\\ c\\ d\\ d')^{\\mathrm{symm}} = e^{\\mathrm{symm}} $$$

Lean4

@[simp, mfld_simps]
theorem mk_symm (e : PartialEquiv H E) (a b c d d') :
    (ModelWithCorners.mk e a b c d d' : ModelWithCorners 𝕜 E H).symm = e.symm :=
  rfl

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