vsub_right_mem_direction_iff_mem — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Given a point in an affine subspace, a result of subtracting that point on the right is in the
direction if and only if the other point is in the subspace. -/
theorem vsub_right_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_right hp]
  simp

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