coe_eq_bot_iff

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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

English

For any affine subspace Q, its underlying set is empty if and only if Q equals the bottom.

Русский

Для любой аффинной подпосности Q множество её точек пусто тогда и только тогда, когда Q = ⊥.

LaTeX

$$$(Q : \mathrm{Set} P) = \varnothing \iff Q = \bot$$$

Lean4

@[simp]
theorem coe_eq_bot_iff (Q : AffineSubspace k P) : (Q : Set P) = ∅ ↔ Q = ⊥ :=
  coe_injective.eq_iff' (bot_coe _ _ _)

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

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

Разделы

Аффилиация

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