sdiff_singleton_nonempty

Mathlib.Data.Finset.SDiff

URI: https://scilib.ai/kg/mathlib#Finset.Nontrivial.sdiff_singleton_nonempty

English

If s is nontrivial, then s \ {c} is nonempty for any c.

Русский

Если у множества s хотя бы два элемента, то s minus {c} непусто.

LaTeX

$$$ |s| \ge 2 \Rightarrow |s \setminus \{c\}| \ge 1 $$$

Lean4

theorem sdiff_singleton_nonempty {c : α} {s : Finset α} (hS : s.Nontrivial) : (s \ { c }).Nonempty := by grind

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

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

Разделы

Аффилиация

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