inf_insert — Mathlib

English

Inserting an element into a finite set does not change the infimum except by taking its meet with the new value.

Русский

Добавление элемента в конечное множество изменяет инфIMUM только через взятие их пересечения с новым значением: inf(insert b s) f = f(b) ⊓ inf s f.

LaTeX

$$$ (\text{insert } b\ s).inf f = f(b) \wedge s.inf f $$$

Lean4

@[simp]
theorem inf_insert [DecidableEq β] {b : β} : (insert b s : Finset β).inf f = f b ⊓ s.inf f :=
  fold_insert_idem

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