isEmpty_left

Mathlib.Logic.IsEmpty

URI: https://scilib.ai/kg/mathlib#Sigma.isEmpty_left

English

If α is empty and E : α → Type*, then the dependent sum Σ a: α, E(a) is empty.

Русский

Если α пуст, то сигма-тип Σ a: α, E(a) пуст.

LaTeX

$$$IsEmpty\left(\Sigma_{a:\\alpha} E(a)\right)$$$

Lean4

instance isEmpty_left {α} [IsEmpty α] {E : α → Type*} : IsEmpty (Sigma E) :=
  Function.isEmpty Sigma.fst

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

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

Разделы

Аффилиация

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