nonempty_of_affineSpan_eq_top

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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

← MathLib Explorer

English

If affineSpan k s = ⊤, then s is nonempty.

Русский

Если аффинная оболочка множества равна ⊤, то множество непусто.

LaTeX

$$affineSpan k s = ⊤ → s.Nonempty$$

Lean4

theorem nonempty_of_affineSpan_eq_top {s : Set P} (h : affineSpan k s = ⊤) : s.Nonempty :=
  by
  rw [Set.nonempty_iff_ne_empty]
  rintro rfl
  rw [AffineSubspace.span_empty] at h
  exact bot_ne_top k V P h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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