# The order on `Prop` #

Instances on `Prop` such as `DistribLattice`, `BoundedOrder`, `LinearOrder`.

source
instance Prop.instDistribLattice :
DistribLattice Prop

Propositions form a distributive lattice.

Equations

- One or more equations did not get rendered due to their size.

source
instance Prop.instBoundedOrder :
BoundedOrder Prop

Propositions form a bounded order.

Equations

- «Prop».instBoundedOrder = { top := True, le_top := ⋯, bot := False, bot_le := @False.elim }

source
@[simp]
theorem Prop.bot_eq_false :
⊥ = False
source
@[simp]
theorem Prop.top_eq_true :
⊤ = True
source
instance Prop.le_isTotal :
IsTotal Prop fun (x1 x2 : Prop) => x1 ≤ x2
source
noncomputable instance Prop.linearOrder :
LinearOrder Prop
Equations

- «Prop».linearOrder = Lattice.toLinearOrder Prop

source
@[simp]
theorem sup_Prop_eq :
(fun (x1 x2 : Prop) => max x1 x2) = fun (x1 x2 : Prop) => x1 ∨ x2
source
@[simp]
theorem inf_Prop_eq :
(fun (x1 x2 : Prop) => min x1 x2) = fun (x1 x2 : Prop) => x1 ∧ x2
source
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)
source
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)
source
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)
source
@[simp]
theorem Prop.disjoint_iff {P Q : Prop} :
Disjoint P Q ↔ ¬(P ∧ Q)
source
@[simp]
theorem Prop.codisjoint_iff {P Q : Prop} :
Codisjoint P Q ↔ P ∨ Q
source
@[simp]
theorem Prop.isCompl_iff {P Q : Prop} :
IsCompl P Q ↔ ¬(P ↔ Q)
source
instance Prop.decidablePredBot {α : Type u} :
DecidablePred ⊥
Equations

- «Prop».decidablePredBot x✝ = instDecidableFalse

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

- «Prop».decidablePredTop x✝ = instDecidableTrue

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

- «Prop».decidableRelBot x✝¹ x✝ = instDecidableFalse

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

- «Prop».decidableRelTop x✝¹ x✝ = instDecidableTrue