subset_singleton_iff

Mathlib.Data.Finset.Insert

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

English

A Finset s is contained in the singleton {a} iff s is empty or s = {a}.

Русский

Финсет s содержится в {a} тогда и только тогда, когда s пуст или s = {a}.

LaTeX

$$$s \subseteq \{ a \} \iff s = \emptyset \lor s = \{ a \}$$$

Lean4

@[simp]
theorem subset_singleton_iff {s : Finset α} {a : α} : s ⊆ { a } ↔ s = ∅ ∨ s = { a } := by grind

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

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

Разделы

Аффилиация

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