isEmpty_of_subsingleton

Mathlib.LinearAlgebra.Projectivization.Cardinality

URI: https://scilib.ai/kg/mathlib#Projectivization.isEmpty_of_subsingleton

← MathLib Explorer

English

If V is a subsingleton, then ℙ_k(V) is empty.

Русский

Если V — одиночное множество, то ℙ_k(V) пусто.

LaTeX

$$[Subsingleton V] ⇒ IsEmpty (ℙ_k(V))$$

Lean4

instance isEmpty_of_subsingleton [Subsingleton V] : IsEmpty (ℙ k V) :=
  by
  have : IsEmpty { v : V // v ≠ 0 } := ⟨fun v ↦ v.2 (Subsingleton.elim v.1 0)⟩
  simpa using (nonZeroEquivProjectivizationProdUnits k V).symm.isEmpty

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

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

Разделы

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

Аффилиация

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