apply_eq_iff_eq

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

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

English

Equality of images of two points under e is equivalent to equality of the points.

Русский

Равенство изображений e(p1) и e(p2) эквивалентно равенству p1 и p2.

LaTeX

$$$e(p_1)=e(p_2) \iff p_1=p_2$$$

Lean4

theorem apply_eq_iff_eq (e : P₁ ≃ᵃ[k] P₂) {p₁ p₂ : P₁} : e p₁ = e p₂ ↔ p₁ = p₂ := by simp

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

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

Разделы

Аффилиация

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