nonempty_of_ne_empty

Mathlib.Data.Finset.Empty

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

English

From the fact that s ≠ ∅, we obtain s.Nonempty.

Русский

Из того, что s ≠ ∅, следует s.Nonempty.

LaTeX

$$$(s \\neq \\emptyset) \\\\Rightarrow s \\\\text{Nonempty}$$$

Lean4

theorem nonempty_of_ne_empty {s : Finset α} (h : s ≠ ∅) : s.Nonempty :=
  exists_mem_of_ne_zero (mt val_eq_zero.1 h)

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

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

Разделы

Аффилиация

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