coe_direction_eq_vsub_set — Mathlib

English

The set of vectors in the direction equals the set of differences between pairs of points in the subspace.

Русский

Множество векторов в направлении равно множеству разностей между парами точек в подпространстве.

LaTeX

$$$(s.direction : Set\\ V) = (s : Set\\ P) -\\vec{} s$$$

Lean4

/-- The set of vectors in the direction of a nonempty affine subspace is given by `vsub_set`. -/
theorem coe_direction_eq_vsub_set {s : AffineSubspace k P} (h : (s : Set P).Nonempty) :
    (s.direction : Set V) = (s : Set P) -ᵥ s :=
  directionOfNonempty_eq_direction h ▸ rfl

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