isEmpty_of_forall_eq_empty

Mathlib.Data.Finset.Basic

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

English

If every Finset s equals ∅, then α is empty.

Русский

Если каждый финсет s равен ∅, то α пуст.

LaTeX

$$$ (H : \\\\forall s : \\\\mathrm{Finset} \\\\alpha, s = \\\\emptyset) \\\\Rightarrow \\\\mathrm{IsEmpty} \\\\alpha $$$

Lean4

theorem isEmpty_of_forall_eq_empty (H : ∀ s : Finset α, s = ∅) : IsEmpty α :=
  isEmpty_iff.mpr fun a ↦ by specialize H { a }; aesop

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

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

Разделы

Аффилиация

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