Theorems · Definition · order theory

conditionallyCompleteLatticeOfLatticeOfsSup

(α : Type u_5) →
  [H1 : Lattice α] →
    [inst : SupSet α] → (∀ (s : Set α), BddAbove s → s.Nonempty → IsLUB s (sSup s)) → ConditionallyCompleteLattice α

A version of conditionallyCompleteLatticeOfsSup when we already know that α is a lattice. This should only be used when it is both hard and unnecessary to provide sInf explicitly.

Defined in

Mathlib.Order.ConditionallyCompleteLattice.Defs

Cited by

0 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LatticeSupSet