Theorems · Theorem · order theory

DirectedOn.csInf_lt_of_lt

∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderInf α] {s : Set α} {a b : α},
  DirectedOn (fun x1 x2 => x2 ≤ x1) s → BddBelow s → a ∈ s → a < b → sInf s < b

sInf s < b when there is an element a in s with a < b, when s is bounded below. This is essentially an iff, except that the assumptions for the two implications are slightly different (one needs boundedness below for one direction, nonemptiness and linear order for the other one), so we formulate separately the two implications, contrary to the CompleteLattice case.

Defined in

Mathlib.Order.ConditionallyCompletePartialOrder.Basic

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

ConditionallyCompletePartialOrderInf