coe_pointwise_vadd — Mathlib

English

The translated subspace equals the image of the translated set under the corresponding affine equivalence.

Русский

Тождество между переносом подпространства и образом переноса множества через соответствующее аффинное отображение.

LaTeX

$$$((v +\!\!\! s) : \mathrm{AffineSubspace}) = s.map (\mathrm{AffineEquiv}.constVAdd k P v).$$$

Lean4

@[simp, norm_cast]
theorem coe_pointwise_vadd (v : V) (s : AffineSubspace k P) :
    ((v +ᵥ s : AffineSubspace k P) : Set P) = v +ᵥ (s : Set P) :=
  rfl

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