instIsEmpty

Mathlib.Logic.IsEmpty

URI: https://scilib.ai/kg/mathlib#Quot.instIsEmpty

English

The quotient by any relation r is empty if the underlying type is empty.

Русский

Квоты по любой relation r пусты, если базовый тип пуст.

LaTeX

$$$ [IsEmpty(\alpha)] {r} : IsEmpty(\mathrm{Quot}(r)) $$$

Lean4

instance instIsEmpty {α : Sort*} [IsEmpty α] {r : α → α → Prop} : IsEmpty (Quot r) :=
  Function.Surjective.isEmpty Quot.exists_rep

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

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

Разделы

Аффилиация

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