The order on Prop

Instances on Prop such as DistribLattice, BoundedOrder, LinearOrder.

instance Prop.distribLattice : DistribLattice Prop

Propositions form a distributive lattice.

Equations

• Prop.distribLattice = DistribLattice.mk Prop.distribLattice.proof_3

instance Prop.boundedOrder : BoundedOrder Prop

Propositions form a bounded order.

Equations

• Prop.boundedOrder = BoundedOrder.mk

theorem Prop.bot_eq_false : ⊥ = False

theorem Prop.top_eq_true : ⊤ = True

instance Prop.le_isTotal : IsTotal Prop fun (x x_1 : Prop) => x ≤ x_1

Equations

• Prop.le_isTotal = (_ : IsTotal Prop fun (x x_1 : Prop) => x ≤ x_1)

noncomputable instance Prop.linearOrder : LinearOrder Prop

Equations

• Prop.linearOrder = Lattice.toLinearOrder Prop

@[simp]

theorem sup_Prop_eq : (fun (x x_1 : Prop) => x ⊔ x_1) = fun (x x_1 : Prop) => x ∨ x_1

@[simp]

theorem inf_Prop_eq : (fun (x x_1 : Prop) => x ⊓ x_1) = fun (x x_1 : Prop) => x ∧ x_1

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} : 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 : (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} : Codisjoint P Q ↔ P ∨ Q

@[simp]

theorem Prop.isCompl_iff {P : Prop} {Q : Prop} : IsCompl P Q ↔ ¬(P ↔ Q)

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

Equations

• Prop.decidablePredBot x = instDecidableFalse

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

Equations

• Prop.decidablePredTop x = instDecidableTrue

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

Equations

• Prop.decidableRelBot x✝ x = instDecidableFalse

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

Equations

• Prop.decidableRelTop x✝ x = instDecidableTrue