coe_pair

Mathlib.Data.Finset.Insert

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

English

The underlying set of the finite set {a, b} is exactly {a, b}.

Русский

Вещественная оболочка конечного множества {a, b} равна точно {a, b}.

LaTeX

$$$\\bigl(({a,b} : \\mathrm{Finset}\\ \\alpha) : \\mathrm{Set}\\ \\alpha\\bigr) = \\{a,b\\}$$$

Lean4

@[norm_cast]
theorem coe_pair {a b : α} : (({ a, b } : Finset α) : Set α) = { a, b } := by grind

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

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

Разделы

Аффилиация

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