Documentation

Mathlib.Order.PropInstances

The order on Prop #

Instances on Prop such as DistribLattice, BoundedOrder, LinearOrder.

source
instance Prop.instDistribLattice :
DistribLattice Prop

Propositions form a distributive lattice.

Equations
    source
    instance Prop.instBoundedOrder :
    BoundedOrder Prop

    Propositions form a bounded order.

    Equations
      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
        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
          source
          instance Prop.decidablePredTop {α : Type u} :
          DecidablePred ⊤
          Equations
            source
            instance Prop.decidableRelBot {α : Type u} :
            DecidableRel ⊥
            Equations
              source
              instance Prop.decidableRelTop {α : Type u} :
              DecidableRel ⊤
              Equations