The strict order and decidability on propositions and predicates

In the implication order on Prop, p < q holds exactly when p fails and q holds, so it is decidable whenever both propositions are; mathlib gives Prop its partial order in Order.Basic without either fact. Likewise the pointwise difference p \ q of two decidable predicates is decidable, the sibling of mathlib's Prop.decidablePredBot and Prop.decidablePredTop.

References

• [UPSTREAM] candidate for Mathlib.Order.Basic and Mathlib.Order.PropInstances.

theorem Prop.lt_iff {p q : Prop} : p < q ↔ ¬p ∧ q

@[instance_reducible]

instance Prop.decidableLT {p q : Prop} [Decidable p] [Decidable q] : Decidable (p < q)

Equations

• «Prop».decidableLT = decidable_of_iff (¬p ∧ q) ⋯

@[instance_reducible]

instance Prop.decidablePredSDiff {α : Type u_1} (p q : α → Prop) [DecidablePred p] [DecidablePred q] : DecidablePred (p \ q)

The difference of two decidable predicates is decidable.

Equations

• «Prop».decidablePredSDiff p q x = decidable_of_iff (p x ∧ ¬q x) ⋯