apply_eq_iff_eq_symm_apply

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

URI: https://scilib.ai/kg/mathlib#AffineEquiv.apply_eq_iff_eq_symm_apply

English

Equality of images under e is equivalent to equality of preimages under its inverse.

Русский

Равенство образов под e эквивалентно равенству прообразов под e^{-1}.

LaTeX

$$$e(p_1)=p_2 \iff 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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru