feat(Order/Hom): prove disjoint from order embedding (#12223)

This adds 3 lemmas which state that if you have an order embedding `f` such that `f a₁` and `f a₂` are disjoint/codisjoint/complements, then the same holds for `a₁` and `a₂`.

*Motivation*: For a project described [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Derivations.20on.20Lie.20algebras), I wanted to know that if two Lie ideals are complements as submodules, then they are complements as Lie ideals too. I realized that the correct level of generality was probably in the `Order.Hom.Basic` file.

*Caveats*: I am very much open to golfing/naming/redesign suggestions. Within the modified file, there was already a `Disjoint.map_orderIso` result, but it requires an `OrderIso` (not just a one-way embedding) and it requires a `SemilatticeInf` (whereas my version just uses `PartialOrder`).

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Mathlib/Order/Hom/Basic.lean

@@ -747,6 +747,34 @@ lemma coe_ofIsEmpty [IsEmpty α] : (ofIsEmpty : α ↪o β) = (isEmptyElim : α
 
 end OrderEmbedding
 
+section Disjoint
+
+variable [PartialOrder α] [PartialOrder β] (f : OrderEmbedding α β)
+
+/-- If the images by an order embedding of two elements are disjoint,
+then they are themselves disjoint. -/
+lemma Disjoint.of_orderEmbedding [OrderBot α] [OrderBot β] {a₁ a₂ : α} :
+    Disjoint (f a₁) (f a₂) → Disjoint a₁ a₂ := by
+  intro h x h₁ h₂
+  rw [← f.le_iff_le] at h₁ h₂ ⊢
+  calc
+    f x ≤ ⊥ := h h₁ h₂
+    _ ≤ f ⊥ := bot_le
+
+/-- If the images by an order embedding of two elements are codisjoint,
+then they are themselves codisjoint. -/
+lemma Codisjoint.of_orderEmbedding [OrderTop α] [OrderTop β] {a₁ a₂ : α} :
+    Codisjoint (f a₁) (f a₂) → Codisjoint a₁ a₂ :=
+  Disjoint.of_orderEmbedding (α := αᵒᵈ) (β := βᵒᵈ) f.dual
+
+/-- If the images by an order embedding of two elements are complements,
+then they are themselves complements. -/
+lemma IsCompl.of_orderEmbedding [BoundedOrder α] [BoundedOrder β] {a₁ a₂ : α} :
+    IsCompl (f a₁) (f a₂) → IsCompl a₁ a₂ := fun ⟨hd, hcd⟩ ↦
+  ⟨Disjoint.of_orderEmbedding f hd, Codisjoint.of_orderEmbedding f hcd⟩
+
+end Disjoint
+
 section RelHom
 
 variable [PartialOrder α] [Preorder β]