injective_sym2

Mathlib.Data.Finset.Sym

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

English

If S.sym2 = T.sym2 then S = T.

Русский

Если S.sym2 = T.sym2, то S = T.

LaTeX

$$$S.sym2 = T.sym2 \Rightarrow S = T$$$

Lean4

theorem injective_sym2 : Function.Injective (Finset.sym2 : Finset α → _) :=
  by
  intro s t h
  ext x
  simpa using congr(s(x, x) ∈ $h)

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

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

Разделы

Аффилиация

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