mathlib3 documentation

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]

def Prop.distrib_lattice :

distrib_lattice Prop

Propositions form a distributive lattice.

Equations

Prop.distrib_lattice = {sup := or, le := partial_order.le Prop.partial_order, lt := partial_order.lt Prop.partial_order, le_refl := Prop.distrib_lattice._proof_1, le_trans := Prop.distrib_lattice._proof_2, lt_iff_le_not_le := Prop.distrib_lattice._proof_3, le_antisymm := Prop.distrib_lattice._proof_4, le_sup_left := or.inl, le_sup_right := or.inr, sup_le := Prop.distrib_lattice._proof_5, inf := and, inf_le_left := and.left, inf_le_right := and.right, le_inf := Prop.distrib_lattice._proof_6, le_sup_inf := Prop.distrib_lattice._proof_7}

@[protected, instance]

def Prop.bounded_order :

bounded_order Prop

Propositions form a bounded order.

Equations

Prop.bounded_order = {top := true, le_top := Prop.bounded_order._proof_1, bot := false, bot_le := false.elim}

theorem Prop.bot_eq_false :

theorem Prop.top_eq_true :

@[protected, instance]

def Prop.le_is_total :

is_total Prop has_le.le

@[protected, instance]

noncomputable def Prop.linear_order :

linear_order Prop

Equations

Prop.linear_order = lattice.to_linear_order Prop

@[simp]

theorem sup_Prop_eq :

has_sup.sup = or

@[simp]

theorem inf_Prop_eq :

has_inf.inf = and

theorem pi.disjoint_iff {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), partial_order (α' i)] [Π (i : ι), order_bot (α' i)] {f g : Π (i : ι), α' i} :

disjoint f 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} :

codisjoint f 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} :

is_compl f g ↔ ∀ (i : ι), is_compl (f i) (g i)

@[simp]

theorem Prop.disjoint_iff {P Q : Prop} :

disjoint P Q ↔ ¬(P ∧ Q)

@[simp]

theorem Prop.codisjoint_iff {P Q : Prop} :

codisjoint P Q ↔ P ∨ Q

@[simp]

theorem Prop.is_compl_iff {P Q : Prop} :

is_compl P Q ↔ ¬(P ↔ Q)