Documentation

Mathlib.Order.PropInstances

The order on Prop #

Instances on Prop such as DistribLattice, BoundedOrder, LinearOrder.

source
@[instance_reducible]
instance Prop.instDistribLattice :
DistribLattice Prop

Propositions form a distributive lattice.

source
@[instance_reducible]
instance Prop.instBoundedOrder :
BoundedOrder Prop

Propositions form a bounded order.

source
@[simp]
theorem Prop.bot_eq_false :
⊥ = False
source
@[simp]
theorem Prop.top_eq_true :
⊤ = True
source
instance Prop.le_total :
Std.Total fun (x1 x2 : Prop) => x1 ≤ x2
source
@[instance_reducible]
noncomputable def Prop.linearOrder :
LinearOrder Prop

The order on Prop is a LinearOrder.

This is not an instance since LinearOrder includes decidability instances, which we want to avoid for Prop.

Instances For
    source
    @[simp]
    theorem sup_Prop_eq :
    (fun (x1 x2 : Prop) => x1 ⊔ x2) = fun (x1 x2 : Prop) => x1 ∨ x2
    source
    @[simp]
    theorem inf_Prop_eq :
    (fun (x1 x2 : Prop) => x1 ⊓ x2) = fun (x1 x2 : Prop) => x1 ∧ x2
    source
    theorem Pi.disjoint_iff {ι : Type u_1} {α' : ι → Type u_3} [(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_3} [(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_3} [(i : ι) → PartialOrder (α' i)] [(i : ι) → BoundedOrder (α' i)] {f g : (i : ι) → α' i} :
    IsCompl f g ↔ ∀ (i : ι), IsCompl (f i) (g i)
    source
    instance Pi.instSymmTopForallForallProp (α : Type u_4) :
    Std.Symm ⊤
    source
    instance Pi.instSymmBotForallForallProp (α : Type u_4) :
    Std.Symm ⊥
    source
    theorem Pi.eq_top_iff_refl_of_subsingleton {α : Type u_2} [Subsingleton α] {r : α → α → Prop} :
    r = ⊤ ↔ Std.Refl r
    source
    theorem Pi.eq_bot_iff_irrefl_of_subsingleton {α : Type u_2} [Subsingleton α] {r : α → α → Prop} :
    r = ⊥ ↔ Std.Irrefl r
    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_reducible]
    instance Prop.decidablePredBot {α : Type u} :
    DecidablePred ⊥
    source
    @[instance_reducible]
    instance Prop.decidablePredTop {α : Type u} :
    DecidablePred ⊤
    source
    @[instance_reducible]
    instance Prop.decidableRelBot {α : Type u} :
    DecidableRel ⊥
    source
    @[instance_reducible]
    instance Prop.decidableRelTop {α : Type u} :
    DecidableRel ⊤