sup_insert

Mathlib.Data.Finset.Lattice.Fold

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

English

For any b, inserting b into S yields (insert b S).sup f = f(b) ⊔ S.sup f.

Русский

Для любого b добавление в S даёт (insert b S).sup f = f(b) ⊔ S.sup f.

LaTeX

$$$ (\\text{insert } b\, s).sup f = f b \\;\\sqcup\\; s.sup f $$$

Lean4

@[simp]
theorem sup_insert [DecidableEq β] {b : β} : (insert b s : Finset β).sup f = f b ⊔ s.sup f :=
  fold_insert_idem

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

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

Разделы

Аффилиация

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