feat(order/symm_diff): Heyting bi-implication (#16544)

Define `bihimp`, the Heyting bi-implication operator. This is dual to `symm_diff` and generalizes `iff` on propositions.

Delete `order.imp` as all the material there is now fully superseded by the Heyting algebra material (`himp`, defined in `order.heyting.basic`).

Author: YaelDillies

src/order/boolean_algebra.lean

@@ -542,8 +542,13 @@ instance : boolean_algebra αᵒᵈ :=
 @[simp] lemma sup_inf_inf_compl : (x ⊓ y) ⊔ (x ⊓ yᶜ) = x :=
 by rw [← sdiff_eq, sup_inf_sdiff _ _]
 
-@[simp] lemma compl_sdiff : (x \ y)ᶜ = xᶜ ⊔ y :=
-by rw [sdiff_eq, compl_inf, compl_compl]
+@[simp] lemma compl_sdiff : (x \ y)ᶜ = x ⇨ y :=
+by rw [sdiff_eq, himp_eq, compl_inf, compl_compl, sup_comm]
+
+@[simp] lemma compl_himp : (x ⇨ y)ᶜ = x \ y := @compl_sdiff αᵒᵈ _ _ _
+
+@[simp] lemma compl_sdiff_compl : xᶜ \ yᶜ = y \ x := by rw [sdiff_compl, sdiff_eq, inf_comm]
+@[simp] lemma compl_himp_compl : xᶜ ⇨ yᶜ = y ⇨ x := @compl_sdiff_compl αᵒᵈ _ _ _
 
 lemma disjoint_compl_left_iff : disjoint xᶜ y ↔ y ≤ x :=
 by rw [←le_compl_iff_disjoint_left, compl_compl]

src/order/bounded_order.lean

@@ -1660,6 +1660,9 @@ section is_compl
 (disjoint : disjoint x y)
 (codisjoint : codisjoint x y)
 
+lemma is_compl_iff [lattice α] [bounded_order α] {a b : α} :
+  is_compl a b ↔ disjoint a b ∧ codisjoint a b := ⟨λ h, ⟨h.1, h.2⟩, λ h, ⟨h.1, h.2⟩⟩
+
 namespace is_compl
 
 section bounded_order

src/order/heyting/basic.lean

@@ -259,6 +259,8 @@ end
 -- `p → q → r ↔ q → p → r`
 lemma himp_left_comm (a b c : α) : a ⇨ b ⇨ c = b ⇨ a ⇨ c := by simp_rw [himp_himp, inf_comm]
 
+@[simp] lemma himp_idem : b ⇨ b ⇨ a = b ⇨ a := by rw [himp_himp, inf_idem]
+
 lemma himp_inf_distrib (a b c : α) : a ⇨ b ⊓ c = (a ⇨ b) ⊓ (a ⇨ c) :=
 eq_of_forall_le_iff $ λ d, by simp_rw [le_himp_iff, le_inf_iff, le_himp_iff]