sup'_insert — Mathlib

English

For a nonempty Finset s and b with a decidable equality, inserting b yields (insert b s).sup' f = f(b) ⊔ s.sup' H f.

Русский

При вставке элемента b в непустое Finset s имеем sup' при вставке: sup' (insert b s) f = f(b) ⊔ sup' s.

LaTeX

$$$ (insert b s).sup' (insert_nonempty _ _) f = f b \;⊔\; s.sup' H f $$$

Lean4

@[simp]
theorem sup'_insert [DecidableEq β] {b : β} : (insert b s).sup' (insert_nonempty _ _) f = f b ⊔ s.sup' H f :=
  by
  rw [← WithBot.coe_eq_coe]
  simp [WithBot.coe_sup]

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