of_orderEmbedding — Mathlib

English

If an order embedding maps two elements to complements, then the original elements are complements.

Русский

Если отображение по порядку переводит два элемента в дополнения, то сами элементы — дополнения.

LaTeX

$$$\forall a_1,a_2:\alpha:\ IsCompl( f(a_1), f(a_2)) \Rightarrow IsCompl(a_1,a_2)$$$

Lean4

/-- If the images by an order embedding of two elements are complements,
then they are themselves complements. -/
theorem 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⟩

Похожие утверждения