csInf_insert — Mathlib

English

The infimum of insert a s is the minimum of a and the infimum of s, provided s is nonempty and bounded below.

Русский

Infimum вставки элемента a в множество s равен минимуму из a и Infimum s, если s непусто и ограничено снизу.

LaTeX

$$$\forall s:\\text{Set }\alpha,\forall a:\\alpha,\ BddBelow\ s \\to s.Nonempty \\to sInf(\text{insert } a\ s) = a \sqcap sInf s$$$

Lean4

/-- The infimum of `insert a s` is the minimum of `a` and the infimum of `s`, if `s` is
nonempty and bounded below. -/
@[simp]
theorem csInf_insert (hs : BddBelow s) (sne : s.Nonempty) : sInf (insert a s) = a ⊓ sInf s :=
  csSup_insert (α := αᵒᵈ) hs sne

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