sup'_cons — Mathlib

English

Let s be a Finset β with H nonempty and f : β → α. If b ∉ s, then the supremum over cons b s equals f(b) ⊔ (sup' over s).

Русский

Пусть s — конечное множество; если b не в s, то sup' по {b}∪s равен f(b) ⊔ sup'(s).

LaTeX

$$$ (\text{cons } b\ s\ hb).sup' (cons_nonempty hb) f = f b \;⊔\; s.sup' H f $$$

Lean4

@[simp]
theorem sup'_cons {b : β} {hb : b ∉ s} : (cons b s hb).sup' (cons_nonempty hb) f = f b ⊔ s.sup' H f :=
  by
  rw [← WithBot.coe_eq_coe]
  simp [WithBot.coe_sup]

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