Order definitions for propositions

This file defines orders on Pi and Prop.

@[implicit_reducible]

instance Pi.hasLe {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → LE (π i)] : LE ((i : ι) → π i)

Equations

• Pi.hasLe = { le := fun (x y : (i : ι) → π i) => ∀ (i : ι), x i ≤ y i }

theorem Pi.le_def {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → LE (π i)] {x y : (i : ι) → π i} : x ≤ y ↔ ∀ (i : ι), x i ≤ y i

@[implicit_reducible]

instance Prop.le : LE Prop

Propositions form a complete Boolean algebra, where the ≤ relation is given by implication.

Equations

• «Prop».le = { le := fun (x1 x2 : Prop) => x1 → x2 }

@[simp]

theorem le_Prop_eq : (fun (x1 x2 : Prop) => x1 ≤ x2) = fun (x1 x2 : Prop) => x1 → x2