mem_direction_iff_eq_vsub_left — Mathlib

English

Two affine subspaces are equal if they have the same members.

Русский

Два аффинных подпространства равны, если их элементы совпадают.

LaTeX

$$$\\forall p,q:\\ AffineSubspace k P, (\\forall x, 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 left. -/
theorem mem_direction_iff_eq_vsub_left {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_left hp]
  exact ⟨fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩, fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩⟩

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