toFinset_nonempty

Mathlib.Data.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Multiset.toFinset_nonempty

English

A multiset has a nonempty toFinset if and only if it is nonzero.

Русский

Мультисет имеет непустой toFinset тогда и только тогда, когда он не равен 0.

LaTeX

$$$\\operatorname{toFinset\\,nonempty}(s) \\leftrightarrow s \\neq 0$$$

Lean4

@[simp]
theorem toFinset_nonempty : s.toFinset.Nonempty ↔ s ≠ 0 := by
  simp only [toFinset_eq_empty, Ne, Finset.nonempty_iff_ne_empty]

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

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

Разделы

Аффилиация

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