inf'_cons — Mathlib

English

If b is not in s, then the infimum of f over the set {b} ∪ s equals the infimum of f over s, joined with f(b) by the infimum operation: inf'({b} ∪ s) f = f(b) ⊓ inf' (s) f.

Русский

Если b не принадлежит s, то инфимум над {b} ∪ s равен f(b) ∧ инфимум над s; то есть инф'_cons.

LaTeX

$$$\\inf'({b}\\cup s) f = f(b) \\wedge \\inf'(s) f$$$

Lean4

@[simp]
theorem inf'_cons {b : β} {hb : b ∉ s} : (cons b s hb).inf' (cons_nonempty hb) f = f b ⊓ s.inf' H f :=
  @sup'_cons αᵒᵈ _ _ _ H f _ _

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