mk_zero

Mathlib.Data.Finset.Empty

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

English

The finite set constructed as ⟨0, nodup_zero⟩ is equal to the empty Finset.

Русский

Конструкция ⟨0, nodup_zero⟩ совпадает с пустым Finset.

LaTeX

$$$ (\\\\langle 0, \\\\mathtt{nodup\_zero} \\\\rangle : Finset\\\\alpha) = \\\\emptyset $$$

Lean4

@[simp]
theorem mk_zero : (⟨0, nodup_zero⟩ : Finset α) = ∅ :=
  rfl

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

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

Разделы

Аффилиация

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