coe_vsub — Mathlib

English

The coercion of the subspace vsub to the ambient vsub is the same as the ambient vsub when viewed in the ambient space.

Русский

Сведение в подпространство через vsub совпадает с соотнесенным векторным различием в окружающем пространстве.

LaTeX

$$$\forall s:\,\text{AffineSubspace},\ [s]\rightarrow\mathbb{N},\; \forall a,b: s,\ ↑(a -ᵥ b) = (a : P) -ᵥ (b : P)$$$

Lean4

@[simp, norm_cast]
theorem coe_vsub (s : AffineSubspace k P) [Nonempty s] (a b : s) : ↑(a -ᵥ b) = (a : P) -ᵥ (b : P) :=
  rfl

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