singleton_subset_iff

Mathlib.Data.Finset.Insert

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

English

A Finset singleton {a} is contained in s as a Finset iff a ∈ s.

Русский

Финсет {a} принадлежит s как Finset тогда и только тогда, когда a ∈ s.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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