The order on Prop

Instances on Prop such as DistribLattice, BoundedOrder, LinearOrder.

instance Prop.instDistribLattice : DistribLattice Prop

Propositions form a distributive lattice.

Equations

• «Prop».instDistribLattice = DistribLattice.mk «Prop».instDistribLattice.proof_3

instance Prop.instBoundedOrder : BoundedOrder Prop

Propositions form a bounded order.

Equations

• «Prop».instBoundedOrder = BoundedOrder.mk

@[simp]

theorem Prop.bot_eq_false : ⊥ = False

@[simp]

theorem Prop.top_eq_true : ⊤ = True

instance Prop.le_isTotal : IsTotal Prop fun (x1 x2 : Prop) => x1 ≤ x2

Equations

• «Prop».le_isTotal = ⋯

noncomputable instance Prop.linearOrder : LinearOrder Prop

Equations

• «Prop».linearOrder = Lattice.toLinearOrder Prop

@[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} : 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