order.imp

# Implication and equivalence as operations on a boolean algebra #

In this file we define lattice.imp (notation: a ⇒ₒ b) and lattice.biimp (notation: a ⇔ₒ b) to be the implication and equivalence as operations on a boolean algebra. More precisely, we put a ⇒ₒ b = aᶜ ⊔ b and a ⇔ₒ b = (a ⇒ₒ b) ⊓ (b ⇒ₒ a). Equivalently, a ⇒ₒ b = (a \ b)ᶜ and a ⇔ₒ b = (a ∆ b)ᶜ. For propositions these operations are equal to the usual implication and iff.

def lattice.imp {α : Type u_1} [has_compl α] [has_sup α] (a b : α) :
α

Implication as a binary operation on a boolean algebra.

Equations
def lattice.biimp {α : Type u_1} [has_compl α] [has_sup α] [has_inf α] (a b : α) :
α

Equivalence as a binary operation on a boolean algebra.

Equations
@[simp]
theorem lattice.imp_eq_arrow (p q : Prop) :
p ⇒ₒ q = (p → q)
@[simp]
theorem lattice.biimp_eq_iff (p q : Prop) :
p ⇔ₒ q = (p q)
@[simp]
theorem lattice.compl_imp {α : Type u_1} (a b : α) :
(a ⇒ₒ b) = a \ b
theorem lattice.compl_sdiff {α : Type u_1} (a b : α) :
(a \ b) = a ⇒ₒ b
theorem lattice.imp_mono {α : Type u_1} {a b c d : α} (h₁ : a b) (h₂ : c d) :
b ⇒ₒ c a ⇒ₒ d
theorem lattice.inf_imp_eq {α : Type u_1} (a b c : α) :
a (b ⇒ₒ c) = a ⇒ₒ b ⇒ₒ a c
@[simp]
theorem lattice.imp_eq_top_iff {α : Type u_1} {a b : α} :
a ⇒ₒ b = a b
@[simp]
theorem lattice.imp_eq_bot_iff {α : Type u_1} {a b : α} :
a ⇒ₒ b = a = b =
@[simp]
theorem lattice.imp_bot {α : Type u_1} (a : α) :
@[simp]
theorem lattice.top_imp {α : Type u_1} (a : α) :
@[simp]
theorem lattice.bot_imp {α : Type u_1} (a : α) :
@[simp]
theorem lattice.imp_top {α : Type u_1} (a : α) :
@[simp]
theorem lattice.imp_self {α : Type u_1} (a : α) :
@[simp]
theorem lattice.compl_imp_compl {α : Type u_1} (a b : α) :
theorem lattice.imp_inf_le {α : Type u_1} (a b : α) :
(a ⇒ₒ b) a b
theorem lattice.inf_imp_eq_imp_imp {α : Type u_1} (a b c : α) :
a b ⇒ₒ c = a ⇒ₒ (b ⇒ₒ c)
theorem lattice.le_imp_iff {α : Type u_1} {a b c : α} :
a b ⇒ₒ c a b c
theorem lattice.biimp_mp {α : Type u_1} (a b : α) :
a ⇔ₒ b a ⇒ₒ b
theorem lattice.biimp_mpr {α : Type u_1} (a b : α) :
a ⇔ₒ b b ⇒ₒ a
theorem lattice.biimp_comm {α : Type u_1} (a b : α) :
a ⇔ₒ b = b ⇔ₒ a
@[simp]
theorem lattice.biimp_eq_top_iff {α : Type u_1} {a b : α} :
a ⇔ₒ b = a = b
@[simp]
theorem lattice.biimp_self {α : Type u_1} (a : α) :
theorem lattice.biimp_symm {α : Type u_1} {a b c : α} :
a b ⇔ₒ c a c ⇔ₒ b
theorem lattice.compl_symm_diff {α : Type u_1} (a b : α) :
(a b) = a ⇔ₒ b
theorem lattice.compl_biimp {α : Type u_1} (a b : α) :
(a ⇔ₒ b) = a b
@[simp]
theorem lattice.compl_biimp_compl {α : Type u_1} {a b : α} :