ssubset_iff_exists_subset_erase

Mathlib.Data.Finset.Basic

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

English

For any a ∈ s, (s.erase a).Nonempty iff s is nontrivial.

Русский

Для любого a ∈ s, (s.erase a).Nonempty тогда и только тогда, когда s не тривиально.

LaTeX

$$$$ (\forall a ∈ s, (s.erase a).\mathrm{Nonempty}) \iff s.\mathrm{Nontrivial}. $$$$

Lean4

theorem ssubset_iff_exists_subset_erase {s t : Finset α} : s ⊂ t ↔ ∃ a ∈ t, s ⊆ t.erase a := by grind

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

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

Разделы

Аффилиация

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