instLawfulSingleton

Mathlib.Data.Finset.Insert

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

English

Finset α with insert is a LawfulSingleton, i.e., insert a ∅ = {a}.

Русский

Множество Finset α с операцией вставки образует законное одноэлементное множество: insert a ∅ = {a}.

LaTeX

$$$\text{instLawfulSingleton}: \forall a, insert\ a\ (\emptyset) = {a}$$$

Lean4

instance : LawfulSingleton α (Finset α) :=
  ⟨fun a => by simp⟩

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

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

Разделы

Аффилиация

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