ne_empty

Mathlib.Data.Finset.Empty

URI: https://scilib.ai/kg/mathlib#Finset.Nonempty.ne_empty

English

From a nonempty Finset, it follows that it is not empty.

Русский

Из непустого Finset следует, что он не пуст.

LaTeX

$$$s \\neq \\emptyset \\Rightarrow s \\neq \\emptyset$$$

Lean4

theorem ne_empty {s : Finset α} (h : s.Nonempty) : s ≠ ∅ :=
  (Exists.elim h) fun _a => ne_empty_of_mem

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

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

Разделы

Аффилиация

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