The order on Prop#

Instances on Prop such as DistribLattice, BoundedOrder, LinearOrder.

Propositions form a distributive lattice.

Equations

Propositions form a bounded order.

Equations
@[simp]
@[simp]
instance Prop.le_isTotal :
IsTotal Prop fun (x1 x2 : Prop) => x1 x2
Equations
noncomputable instance Prop.linearOrder :
Equations
@[simp]
theorem sup_Prop_eq :
(fun (x1 x2 : Prop) => x1 x2) = fun (x1 x2 : Prop) => x1 x2
@[simp]
theorem inf_Prop_eq :
(fun (x1 x2 : Prop) => x1 x2) = fun (x1 x2 : Prop) => x1 x2
theorem Pi.disjoint_iff {ι : Type u_1} {α' : ιType u_2} [(i : ι) → PartialOrder (α' i)] [(i : ι) → OrderBot (α' i)] {f : (i : ι) → α' i} {g : (i : ι) → α' i} :
Disjoint f g ∀ (i : ι), Disjoint (f i) (g i)
theorem Pi.codisjoint_iff {ι : Type u_1} {α' : ιType u_2} [(i : ι) → PartialOrder (α' i)] [(i : ι) → OrderTop (α' i)] {f : (i : ι) → α' i} {g : (i : ι) → α' i} :
∀ (i : ι), Codisjoint (f i) (g i)
theorem Pi.isCompl_iff {ι : Type u_1} {α' : ιType u_2} [(i : ι) → PartialOrder (α' i)] [(i : ι) → BoundedOrder (α' i)] {f : (i : ι) → α' i} {g : (i : ι) → α' i} :
IsCompl f g ∀ (i : ι), IsCompl (f i) (g i)
@[simp]
theorem Prop.disjoint_iff {P : Prop} {Q : Prop} :
Disjoint P Q ¬(P Q)
@[simp]
theorem Prop.codisjoint_iff {P : Prop} {Q : Prop} :
P Q
@[simp]
theorem Prop.isCompl_iff {P : Prop} {Q : Prop} :
IsCompl P Q ¬(P Q)
instance Prop.decidablePredBot {α : Type u} :
Equations
instance Prop.decidablePredTop {α : Type u} :
Equations
instance Prop.decidableRelBot {α : Type u} :
Equations
instance Prop.decidableRelTop {α : Type u} :
Equations