nonempty_coe_sort

Mathlib.Data.Finset.Empty

URI: https://scilib.ai/kg/mathlib#Finset.nonempty_coe_sort

English

Let s be a finite set. The type of its elements is inhabited if and only if s is nonempty.

Русский

Пусть s — конечное множество. Тип элементов s непуст, если и только если s непусто.

LaTeX

$$$\\\\exists x \\\\in s \\\\iff s \\\\neq \\\\emptyset$$$

Lean4

theorem nonempty_coe_sort {s : Finset α} : Nonempty (s : Type _) ↔ s.Nonempty :=
  nonempty_subtype

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

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

Разделы

Аффилиация

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