apply_eq_iff_eq

Mathlib.Topology.Algebra.ContinuousAffineEquiv

URI: https://scilib.ai/kg/mathlib#ContinuousAffineEquiv.apply_eq_iff_eq

English

For e, e.symm (e p) = p.

Русский

Для э и p верно: e.symm (e p) = p.

LaTeX

$$$ e.\\mathrm{symm}(e(p)) = p $$$

Lean4

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

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

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

Разделы

Аффилиация

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