vadd_mem_pointwise_vadd_iff

Mathlib.LinearAlgebra.AffineSpace.Pointwise

URI: https://scilib.ai/kg/mathlib#AffineSubspace.vadd_mem_pointwise_vadd_iff

English

v + p ∈ v + s if and only if p ∈ s.

Русский

Пусть v — вектор, p ∈ s тогда v + p ∈ v + s и наоборот.

LaTeX

$$$v + p \in v + s \iff p \in s.$$$

Lean4

theorem vadd_mem_pointwise_vadd_iff {v : V} {s : AffineSubspace k P} {p : P} : v +ᵥ p ∈ v +ᵥ s ↔ p ∈ s :=
  vadd_mem_vadd_set_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru