English
If f is an order embedding, and f(a1) and f(a2) are disjoint in β, then a1 and a2 are disjoint in α, provided α and β have bottom elements.
Русский
Если f — вложение по порядку и образы a1, a2 в β имеют общую нижнюю границу, то сами a1, a2 в α также несовместны, при условии существования нуля.
LaTeX
$$$\forall a_1,a_2:\alpha:\ Disjoint( f(a_1), f(a_2)) \Rightarrow Disjoint(a_1,a_2)$$$
Lean4
/-- If the images by an order embedding of two elements are disjoint,
then they are themselves disjoint. -/
theorem 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
