lifts_zero

Mathlib.LinearAlgebra.PiTensorProduct

URI: https://scilib.ai/kg/mathlib#PiTensorProduct.lifts_zero

← MathLib Explorer

English

For every x ∈ ⨂[R] i, s_i there exists a lift; i.e., lifts x is nonempty.

Русский

Для каждого x ∈ ⨂[R] i, s_i существует подъем; то есть lifts x непусто.

LaTeX

$$$$ \text{Set.Nonempty}(\text{lifts}(x)) $$$$

Lean4

/-- The empty list lifts the element `0` of `⨂[R] i, s i`.
-/
theorem lifts_zero : 0 ∈ lifts (0 : ⨂[R] i, s i) := by
  rw [mem_lifts_iff, FreeAddMonoid.toList_zero, List.map_nil, List.sum_nil]

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

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

Разделы

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

Аффилиация

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