sup_cons

Mathlib.Data.Finset.Lattice.Fold

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

English

If b is not in S, then the supremum over (b :: S) equals f(b) ⊔ (sup over S).

Русский

Если b не принадлежит S, то верхняя грань над {b} ∪ S равна f(b) ⊔ sup_S f.

LaTeX

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

Lean4

@[simp]
theorem sup_cons {b : β} (h : b ∉ s) : (cons b s h).sup f = f b ⊔ s.sup f :=
  fold_cons h

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

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

Разделы

Аффилиация

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