notMem_bot

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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

English

No point lies in the bottom affine subspace.

Русский

Нижнее аффинное подпространство не содержит точек.

LaTeX

$$$\forall p \in P,\ p \notin \perp$$$

Lean4

/-- No points are in `⊥`. -/
theorem notMem_bot (p : P) : p ∉ (⊥ : AffineSubspace k P) :=
  Set.notMem_empty p

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

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

Разделы

Аффилиация

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