sym2_eq_mk_image

Mathlib.Data.Sym.Sym2

URI: https://scilib.ai/kg/mathlib#Set.sym2_eq_mk_image

English

The set s.sym2 is equal to the image of s under the constructor mk, paired with s.

Русский

Множество s.sym2 равно образу s под конструктором mk, соединённым с s.

LaTeX

$$$\\forall {s : \\mathrm{Set}(\\alpha)},\\; \\mathrm{sym2}(s) = \\mathrm{Sym2.mk}'' s \\times s$$$

Lean4

theorem sym2_eq_mk_image : s.sym2 = Sym2.mk '' s ×ˢ s := by ext ⟨x, y⟩; aesop

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

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

Разделы

Аффилиация

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