instNonemptyOfNontrivial

Mathlib.LinearAlgebra.Projectivization.Basic

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

English

If V is nontrivial, then the projectivization is nonempty.

Русский

Если V не тривиально, проективное пространство непусто.

LaTeX

$$$ \text{Nonempty}(\mathbb{P}_K V)$$$

Lean4

instance [Nontrivial V] : Nonempty (ℙ K V) :=
  let ⟨v, hv⟩ := exists_ne (0 : V)
  ⟨mk K v hv⟩

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

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

Разделы

Аффилиация

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