vsub_left_mem_direction_iff_mem — Mathlib

English

Let s be an affine subspace and p ∈ s. Then for any p2, p −ᵥ p2 ∈ s.direction iff p2 ∈ s.

Русский

Пусть s – аффинное подпространство, p ∈ s. Тогда для любого p2 верно: p −ᵥ p2 ∈ direction(s) тогда и тогда, когда p2 ∈ s.

LaTeX

$$$p\in s \Rightarrow (p -ᵥ p_2) \in s.direction \iff p_2 \in s$$$

Lean4

/-- Given a point in an affine subspace, a result of subtracting that point on the left is in the
direction if and only if the other point is in the subspace. -/
theorem vsub_left_mem_direction_iff_mem {s : AffineSubspace k P} {p : P} (hp : p ∈ s) (p₂ : P) :
    p -ᵥ p₂ ∈ s.direction ↔ p₂ ∈ s := by
  rw [mem_direction_iff_eq_vsub_left hp]
  simp

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