symm_apply — Mathlib

English

The inverse of the quotient equivalence sends a point in the fundamental domain to its coset in the quotient space.

Русский

Обратная к эквивалентности частного пространства отображает точку из фундаментальной области в её косет в частном пространстве.

LaTeX

$$$(\text{quotientEquiv}(b)).\text{symm}(x) = \operatorname{Quotient.mk}(x).$$$

Lean4

@[simp]
theorem symm_apply [Fintype ι] (x : fundamentalDomain b) : (quotientEquiv b).symm x = Submodule.Quotient.mk ↑x :=
  by
  rw [Equiv.symm_apply_eq, quotientEquiv_apply_mk b ↑x, Subtype.ext_iff, fractRestrict_apply]
  exact (fract_eq_self.mpr x.prop).symm

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