symm_apply_apply — Mathlib

English

The symm_apply_apply property states that applying a map and its inverse returns the original input.

Русский

Свойство symm_apply_apply говорит, что применение отображения и его обратного отображения возвращает исходное значение.

LaTeX

$$$$ e.\text{symm_apply_apply}(x) = x \quad \text{for } x \in P. $$$$

Lean4

@[simp]
theorem symm_apply_apply (x : P) : e.symm (e x) = x :=
  e.toAffineEquiv.symm_apply_apply x

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