isEmpty_coe_sort

Mathlib.Data.Finset.Empty

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

English

The type of elements of s, viewed as a separate type, is empty if and only if s is empty.

Русский

Тип элементов s, рассматриваемый как отдельный тип, пуст тогда, когда s пуст.

LaTeX

$$$ \operatorname{IsEmpty}(s : Type _) \iff s = \emptyset $$$

Lean4

@[simp]
theorem isEmpty_coe_sort {s : Finset α} : IsEmpty (s : Type _) ↔ s = ∅ := by simpa using @Set.isEmpty_coe_sort α s

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

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

Разделы

Аффилиация

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