coe_direction_eq_vsub_set_right — Mathlib

English

For a nonempty s, the set of vectors in its direction equals the image of s under the right subtraction by p.

Русский

Для непустого s множество векторов в направлении равно образу s при правом вычитании на p.

LaTeX

$$$\\forall s:\\ AffineSubspace k P, (s : Set P).Nonempty \\Rightarrow (s.direction : Set V) = \\{ p_2 -ᵥ p : p_2 \\in s, p \\in s \\}$$$

Lean4

/-- Given a point in an affine subspace, the set of vectors in its direction equals the set of
vectors subtracting that point on the right. -/
theorem coe_direction_eq_vsub_set_right {s : AffineSubspace k P} {p : P} (hp : p ∈ s) :
    (s.direction : Set V) = (· -ᵥ p) '' s :=
  by
  rw [coe_direction_eq_vsub_set ⟨p, hp⟩]
  refine le_antisymm ?_ ?_
  · rintro v ⟨p₁, hp₁, p₂, hp₂, rfl⟩
    exact ⟨(p₁ -ᵥ p₂) +ᵥ p, vadd_mem_of_mem_direction (vsub_mem_direction hp₁ hp₂) hp, vadd_vsub _ _⟩
  · rintro v ⟨p₂, hp₂, rfl⟩
    exact ⟨p₂, hp₂, p, hp, rfl⟩

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