feat(order/hom/basic): compl as a dual order isomorphism (#11630)

src/order/hom/basic.lean

@@ -54,11 +54,13 @@ because the more bundled version usually does not work with dot notation.
   `order_dual α →o order_dual β`;
 * `order_hom.dual_iso`: order isomorphism between `α →o β` and
   `order_dual (order_dual α →o order_dual β)`;
+* `order_iso.compl`: order isomorphism `α ≃o order_dual α` given by taking complements in a
+  boolean algebra;
 
 We also define two functions to convert other bundled maps to `α →o β`:
 
 * `order_embedding.to_order_hom`: convert `α ↪o β` to `α →o β`;
-* `rel_hom.to_order_hom`: conver a `rel_hom` between strict orders to a `order_hom`.
+* `rel_hom.to_order_hom`: convert a `rel_hom` between strict orders to a `order_hom`.
 
 ## Tags
 
@@ -687,3 +689,23 @@ theorem order_iso.is_complemented_iff :
 
 end bounded_order
 end lattice_isos
+
+section boolean_algebra
+variables (α) [boolean_algebra α]
+
+/-- Taking complements as an order isomorphism to the order dual. -/
+@[simps]
+def order_iso.compl : α ≃o order_dual α :=
+{ to_fun := order_dual.to_dual ∘ compl,
+  inv_fun := compl ∘ order_dual.of_dual,
+  left_inv := compl_compl,
+  right_inv := compl_compl,
+  map_rel_iff' := λ x y, compl_le_compl_iff_le }
+
+theorem compl_strict_anti : strict_anti (compl : α → α) :=
+(order_iso.compl α).strict_mono
+
+theorem compl_antitone : antitone (compl : α → α) :=
+(order_iso.compl α).monotone
+
+end boolean_algebra