coe_mk

Mathlib.Data.Sym.Sym2

URI: https://scilib.ai/kg/mathlib#Sym2.coe_mk

English

The set s(x,y) is exactly {x, y}.

Русский

Множество s(x,y) равно {x,y}.

LaTeX

$$$ (s(x,y) :\\ Set \\alpha) = \\{ x, y \\}. $$$

Lean4

@[simp]
theorem coe_mk {x y : α} : (s(x, y) : Set α) = { x, y } := by ext z; simp

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

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

Разделы

Аффилиация

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