insert_val_of_notMem

Mathlib.Data.Finset.Insert

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

English

If a ∉ s, then (insert a s).val = a :: s.1.

Русский

Если a ∉ s, то (insert a s).val = a :: s.1.

LaTeX

$$$ (a \notin s) \Rightarrow (insert\,a\,s).1 = a :: s.1 $$$

Lean4

theorem insert_val_of_notMem {a : α} {s : Finset α} (h : a ∉ s) : (insert a s).1 = a ::ₘ s.1 := by
  rw [insert_val, ndinsert_of_notMem h]

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

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

Разделы

Аффилиация

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