mem_toAffineSubspace

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

URI: https://scilib.ai/kg/mathlib#Submodule.mem_toAffineSubspace

English

For any submodule p and vector x, x ∈ p.toAffineSubspace iff x ∈ p.

Русский

Для подмодуля p и вектора x верно: x ∈ p.toAffineSubspace тогда и только тогда, когда x ∈ p.

LaTeX

$$$x \\in p.toAffineSubspace \\iff x \\in p$$$

Lean4

@[simp]
theorem mem_toAffineSubspace {p : Submodule k V} {x : V} : x ∈ p.toAffineSubspace ↔ x ∈ p :=
  Iff.rfl

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

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

Разделы

Аффилиация

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