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
.
@[simp]
theorem
lattice.imp_mono
{α : Type u_1}
[boolean_algebra α]
{a b c d : α}
(h₁ : a ≤ b)
(h₂ : c ≤ d) :
@[simp]
@[simp]
@[simp]
@[simp]