coe_cons

Mathlib.Data.Finset.Insert

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

English

The set underlying cons a s h equals insert a (s : Set α).

Русский

Множество, лежащее в основе cons a s h, равно insert a (s : Set α).

LaTeX

$$@[simp] theorem coe_cons {a s h} : (@cons α a s h : Set α) = insert a (s : Set α)$$

Lean4

@[simp]
theorem coe_cons {a s h} : (@cons α a s h : Set α) = insert a (s : Set α) :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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