The complete lattice of propositions

⊑ is implication and the supremum of a set of propositions is the existential quantifier over it.

The instances are scoped in Std.Internal.Order, outside of Lean.Order. partial_fixpoint and coinductive_fixpoint order Prop by ImplicationOrder and ReverseImplicationOrder, and their monotonicity lemmas live in Lean.Order itself. Open Std.Internal.Order to order Prop by implication.

@[instance_reducible]

def Std.Internal.Order.instPartialOrderProp : Lean.Order.PartialOrder Prop

Equations

• One or more equations did not get rendered due to their size.

def Std.Internal.Order.propSup (c : Prop → Prop) : Prop

Supremum for Prop: true iff some element of the set is true

Equations

• Std.Internal.Order.propSup c = ∃ (p : Prop), c p ∧ p

theorem Std.Internal.Order.propSup_is_sup (c : Prop → Prop) : Lean.Order.is_sup c (propSup c)

@[instance_reducible]

def Std.Internal.Order.instCompleteLatticeProp : Lean.Order.CompleteLattice Prop

Equations

• Std.Internal.Order.instCompleteLatticeProp = { toPartialOrder := Std.Internal.Order.instPartialOrderProp, has_sup := Std.Internal.Order.instCompleteLatticeProp._proof_1 }