mem_direction_iff_eq_vsub_right — Mathlib

English

Affine subspaces are uniquely determined by their point-set: if two subspaces have the same elements, they are equal.

Русский

Аффинные подпространства однозначно определяются своим множеством точек: если у двух подпространств одинаковые элементы, они равны.

LaTeX

$$$\\forall p,q:\\ AffineSubspace k P, (\\forall x:\\ P, x \\in p \\iff x \\in q) \\Rightarrow p = q$$$

Lean4

/-- Given a point in an affine subspace, a vector is in its direction if and only if it results from
subtracting that point on the right. -/
theorem mem_direction_iff_eq_vsub_right {s : AffineSubspace k P} {p : P} (hp : p ∈ s) (v : V) :
    v ∈ s.direction ↔ ∃ p₂ ∈ s, v = p₂ -ᵥ p :=
  by
  rw [← SetLike.mem_coe, coe_direction_eq_vsub_set_right hp]
  exact ⟨fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩, fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩⟩

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