erase_val

Mathlib.Data.Finset.Erase

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

English

The underlying multiset value of erase s a equals the multiset s.1 erased at a.

Русский

Должно быть, что подмножество с erased имеет значение, равное удалению из исходного мультинабора элемента a.

LaTeX

$$$ (erase(s,a)).\text{val} = s.\text{val}.erase(a) $$$

Lean4

@[simp]
theorem erase_val (s : Finset α) (a : α) : (erase s a).1 = s.1.erase a :=
  rfl

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

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

Разделы

Аффилиация

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