coe_eq_univ_iff

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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

English

The underlying set of Q is all of P iff Q equals the top.

Русский

Основанное множество Q равно всему пространству, если Q = ⊤.

LaTeX

$$$(Q : \mathrm{Set} P) = \mathrm{univ} \iff Q = \top$$$

Lean4

@[simp]
theorem coe_eq_univ_iff (Q : AffineSubspace k P) : (Q : Set P) = univ ↔ Q = ⊤ :=
  coe_injective.eq_iff' (top_coe _ _ _)

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

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

Разделы

Аффилиация

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