inf'_insert — Mathlib

English

For any b and hb stating b ∉ s, the infimum over insert b s is f(b) ⊓ inf' (s) f; i.e., the Infimum distributes over insertion.

Русский

Для любого b и hb: b не в s, инфимум над insert b s равен f(b) ∧ инфимум над s.

LaTeX

$$$\\inf' (\\mathrm{insert}\\; b\\; s) f = f(b) \\wedge \\inf'(s) f$$$

Lean4

@[simp]
theorem inf'_insert [DecidableEq β] {b : β} : (insert b s).inf' (insert_nonempty _ _) f = f b ⊓ s.inf' H f :=
  @sup'_insert αᵒᵈ _ _ _ H f _ _

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