mathlib documentation

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.

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

Implication as a binary operation on a boolean algebra.

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

Equivalence as a binary operation on a boolean algebra.

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