nonempty_iff_ne_bot

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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

← MathLib Explorer

English

The underlying set of Q is nonempty if and only if Q is not bottom.

Русский

Множество точек Q непусто тогда и только тогда Q ≠ ⊥.

LaTeX

$$$(Q : \mathrm{Set} P).Nonempty \iff Q \neq \bot$$$

Lean4

theorem nonempty_iff_ne_bot (Q : AffineSubspace k P) : (Q : Set P).Nonempty ↔ Q ≠ ⊥ :=
  by
  rw [nonempty_iff_ne_empty]
  exact not_congr Q.coe_eq_bot_iff

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

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

Разделы

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

Аффилиация

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