The order on Prop

Instances on Prop such as DistribLattice, BoundedOrder, LinearOrder.

@[implicit_reducible]

instance Prop.instDistribLattice : DistribLattice Prop

Propositions form a distributive lattice.

@[implicit_reducible]

instance Prop.instBoundedOrder : BoundedOrder Prop

Propositions form a bounded order.

@[simp]

theorem Prop.bot_eq_false : ⊥ = False

@[simp]

theorem Prop.top_eq_true : ⊤ = True

instance Prop.le_total : Std.Total fun (x1 x2 : Prop) => x1 ≤ x2

@[implicit_reducible]

noncomputable instance Prop.linearOrder : LinearOrder Prop

@[simp]

theorem sup_Prop_eq : (fun (x1 x2 : Prop) => max x1 x2) = fun (x1 x2 : Prop) => x1 ∨ x2

@[simp]

theorem inf_Prop_eq : (fun (x1 x2 : Prop) => min 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 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 g : (i : ι) → α' i} : Codisjoint f g ↔ ∀ (i : ι), Codisjoint (f i) (g i)

theorem Pi.isCompl_iff {ι : Type u_1} {α' : ι → Type u_2} [(i : ι) → PartialOrder (α' i)] [(i : ι) → BoundedOrder (α' i)] {f g : (i : ι) → α' i} : IsCompl f g ↔ ∀ (i : ι), IsCompl (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.isCompl_iff {P Q : Prop} : IsCompl P Q ↔ ¬(P ↔ Q)

@[implicit_reducible]

instance Prop.decidablePredBot {α : Type u} : DecidablePred ⊥

@[implicit_reducible]

instance Prop.decidablePredTop {α : Type u} : DecidablePred ⊤

@[implicit_reducible]

instance Prop.decidableRelBot {α : Type u} : DecidableRel ⊥

@[implicit_reducible]

instance Prop.decidableRelTop {α : Type u} : DecidableRel ⊤