English
Let f be an order-embedding between preordered sets. If f(a) covers f(b) in the codomain, then a covers b in the domain.
Русский
Пусть f является вложением порядка между предобозначенными множествами. Если f(a) покрывает f(b) в кодоме, то a покрывает b в домене.
LaTeX
$$$$\forall \alpha \beta [\text{Preorder }\alpha][\text{Preorder }\beta],\ \forall a,b\in\alpha,\ \forall f:\\alpha\hookrightarrow_{\mathrm{ord}}\beta,\ f(a)\,⩿\, f(b)\Rightarrow a\,⩿\, b.$$$$
Lean4
theorem of_image (f : α ↪o β) (h : f a ⩿ f b) : a ⩿ b :=
⟨f.le_iff_le.mp h.le, fun _ hac hcb => h.2 (f.lt_iff_lt.mpr hac) (f.lt_iff_lt.mpr hcb)⟩
