singleton_subset_set_iff

Mathlib.Data.Finset.Insert

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

English

The singleton {a} is contained in s as a Set if and only if a ∈ s.

Русский

Единственный элемент {a} принадлежит s как множеству тогда и только тогда, когда a ∈ s.

LaTeX

$$$\{ a \} \subseteq (s : Set \alpha) \iff a \in s$$$

Lean4

theorem singleton_subset_set_iff {s : Set α} {a : α} : ↑({ a } : Finset α) ⊆ s ↔ a ∈ s := by grind

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

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

Разделы

Аффилиация

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