HepLean 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
Equations
source
noncomputable instance Prop.linearOrder :
LinearOrder Prop
Equations
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_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