apply_eq_iff_eq_symm_apply — Mathlib

English

For a continuous affine equivalence e, e p1 = p2 if and only if p1 = e.symm p2.

Русский

Для непрерывного аффинного эквивалента e верно: e(p1) = p2 тогда и только тогда, когда p1 = e.symm(p2).

LaTeX

$$$ e(p_1) = p_2 \\Leftrightarrow p_1 = e^{-1}(p_2) $$$

Lean4

theorem apply_eq_iff_eq_symm_apply (e : P₁ ≃ᴬ[k] P₂) {p₁ p₂} : e p₁ = p₂ ↔ p₁ = e.symm p₂ :=
  e.toEquiv.apply_eq_iff_eq_symm_apply

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