val_inj

Mathlib.Data.Finset.Defs

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

English

Equality of the underlying multisets is equivalent to equality of Finsets: s.val = t.val iff s = t.

Русский

Равенство подлежащих мультимножеств эквивалентно равенству Finset: s.val = t.val ⇔ s = t.

LaTeX

$$$ s.\mathrm{val} = t.\mathrm{val} \iff s = t $$$

Lean4

@[simp]
theorem val_inj {s t : Finset α} : s.1 = t.1 ↔ s = t :=
  val_injective.eq_iff

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

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

Разделы

Аффилиация

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