mathlib3documentation

order.prop_instances

The order on Prop#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Instances on Prop such as distrib_lattice, bounded_order, linear_order.

@[protected, instance]

Propositions form a distributive lattice.

Equations
@[protected, instance]

Propositions form a bounded order.

Equations
theorem Prop.top_eq_true  :
@[protected, instance]
@[protected, instance]
noncomputable def Prop.linear_order  :
Equations
@[simp]
theorem sup_Prop_eq  :
@[simp]
theorem inf_Prop_eq  :
theorem pi.disjoint_iff {ι : Type u_1} {α' : ι Type u_2} [Π (i : ι), partial_order (α' i)] [Π (i : ι), order_bot (α' i)] {f g : Π (i : ι), α' i} :
g (i : ι), disjoint (f i) (g i)
theorem pi.codisjoint_iff {ι : Type u_1} {α' : ι Type u_2} [Π (i : ι), partial_order (α' i)] [Π (i : ι), order_top (α' i)] {f g : Π (i : ι), α' i} :
g (i : ι), codisjoint (f i) (g i)
theorem pi.is_compl_iff {ι : Type u_1} {α' : ι Type u_2} [Π (i : ι), partial_order (α' i)] [Π (i : ι), bounded_order (α' i)] {f g : Π (i : ι), α' i} :
g (i : ι), is_compl (f i) (g i)
@[simp]
theorem Prop.disjoint_iff {P Q : Prop} :
Q ¬(P Q)
@[simp]
theorem Prop.codisjoint_iff {P Q : Prop} :
Q P Q
@[simp]
theorem Prop.is_compl_iff {P Q : Prop} :
Q ¬(P Q)