apply_symm_apply — Mathlib

English

Let e be a ContinuousMulEquiv from M to N. Then for every y in N, e(e^{-1}(y)) = y; that is, e followed by its inverse is the identity on N.

Русский

Пусть e — непрерывный мультипликативный эквивалент между M и N. Тогда для каждого y в N выполняется e(e^{-1}(y)) = y; то есть применение e после обратного отображения даёт тождественную отображение на N.

LaTeX

$$$e(e^{-1}(y)) = y \quad \text{for all } y \in N.$$$

Lean4

/-- `e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`. -/
@[to_additive (attr := simp) /-- `e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`. -/
    ]
theorem apply_symm_apply (e : M ≃ₜ* N) (y : N) : e (e.symm y) = y :=
  e.toEquiv.apply_symm_apply y

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