Theorems · Theorem · order theory

ConditionallyCompletePartialOrderInf.isGLB_csInf_of_directed

∀ {α : Type u_3} [self : ConditionallyCompletePartialOrderInf α] (s : Set α),
  DirectedOn (fun x1 x2 => x1 ≥ x2) s → s.Nonempty → BddBelow s → IsGLB s (sInf s)

For each nonempty, directed set s which is bounded below, sInf s is the greatest lower bound of s.

Defined in

Mathlib.Order.ConditionallyCompletePartialOrder.Defs

Cited by

1 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

ConditionallyCompletePartialOrderInf