csInf_univ — Mathlib

English

In a ConditionallyCompleteLattice with a bottom element, the infimum of the whole space equals the bottom element: sInf(univ) = ⊥.

Русский

В условно полноупорядоченной решетке с нулем-верхним, инфимуум всего множества равен нижнему элементу: sInf(univ) = ⊥.

LaTeX

$$$sInf(\mathrm{univ}) = \bot$$$

Lean4

@[simp]
theorem csInf_univ [ConditionallyCompleteLattice α] [OrderBot α] : sInf (univ : Set α) = ⊥ :=
  isLeast_univ.csInf_eq

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