toFinset_mk_eq

Mathlib.Data.Sym.Sym2

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

English

The toFinset of a constructed pair equals the set containing its two elements.

Русский

toFinset(cозданной пары) равно множеству, содержащее два её элемента.

LaTeX

$$$$ \mathrm{toFinset}(\mathrm{Sym2.mk}\{ fst := x, snd := y \}).toFinset = \{ x, y \}. $$$$

Lean4

theorem toFinset_mk_eq {x y : α} : s(x, y).toFinset = { x, y } := by ext; simp [← Sym2.mem_toFinset, ← Sym2.mem_iff]

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

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

Разделы

Аффилиация

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