English
Let f be an order-embedding. If a covers b in the domain, and the range of f is OrdConnected, then f(a) covers f(b) in the codomain.
Русский
Пусть f — вложение порядка. Если a покрывает b в области определения, и образ f имеет свойство OrdConnected, то f(a) покрывает f(b) в областиValue.
LaTeX
$$$$\forall \alpha \beta [\text{Preorder }\alpha][\text{Preorder }\beta],\forall a,b\in\alpha,\forall f:\\alpha\hookrightarrow_{\mathrm{ord}}\beta,\ a\,⩿\, b\Rightarrow (\mathrm{range}(f)).\mathrm{OrdConnected}\Rightarrow f(a)\,⩿\, f(b).$$$$
Lean4
theorem image (f : α ↪o β) (hab : a ⩿ b) (h : (range f).OrdConnected) : f a ⩿ f b :=
by
refine ⟨f.monotone hab.le, fun c ha hb => ?_⟩
obtain ⟨c, rfl⟩ := h.out (mem_range_self _) (mem_range_self _) ⟨ha.le, hb.le⟩
rw [f.lt_iff_lt] at ha hb
exact hab.2 ha hb
