singleton_subset_iff

Mathlib.Data.Set.Insert

URI: https://scilib.ai/kg/mathlib#Set.singleton_subset_iff

English

The singleton {a} is a subset of s iff a ∈ s.

Русский

Подмножество {a} ⊆ s эквивалентно a ∈ s.

LaTeX

$$$\\{ a \\} \\subseteq s \\iff a \\in s$$$

Lean4

@[simp, grind =]
theorem singleton_subset_iff {a : α} {s : Set α} : { a } ⊆ s ↔ a ∈ s :=
  forall_eq

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

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

Разделы

Аффилиация

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