Theorems · Definition · order theory

ConditionallyCompletePartialOrder.recOn

{α : Type u_3} →
  {motive : ConditionallyCompletePartialOrder α → Sort u} →
    (t : ConditionallyCompletePartialOrder α) →
      ([toConditionallyCompletePartialOrderSup : ConditionallyCompletePartialOrderSup α] →
          [toInfSet : InfSet α] →
            (isGLB_csInf_of_directed :
                ∀ (s : Set α), DirectedOn (fun x1 x2 => x1 ≥ x2) s → s.Nonempty → BddBelow s → IsGLB s (sInf s)) →
              motive
                { toConditionallyCompletePartialOrderSup := toConditionallyCompletePartialOrderSup,
                  toInfSet := toInfSet, isGLB_csInf_of_directed := isGLB_csInf_of_directed }) →
        motive t

Defined in

Mathlib.Order.ConditionallyCompletePartialOrder.Defs

Cited by

0 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms