erase_ssubset

Mathlib.Data.Finset.Basic

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

English

If a finite set s is nontrivial, then erasing any element a yields a nonempty set.

Русский

Если конечное множество s не тривиально, то удаление любого элемента a даёт непустое множество.

LaTeX

$$$$ s\text{ nontrivial } \Rightarrow (s\setminus\{a\}) \neq \emptyset. $$$$

Lean4

theorem erase_ssubset {a : α} {s : Finset α} (h : a ∈ s) : s.erase a ⊂ s := by grind

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

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

Разделы

Аффилиация

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