English
Let e be an order isomorphism between α and β. If s is an OrdConnected subset of α, then the image e''s is OrdConnected in β.
Русский
Пусть e является упорядоченным изоморфизмом между множестами α и β. Если s ⊆ α является упорядоченно связным, то образ e''s ⊆ β также упорядоченно связен.
LaTeX
$$$\\forall e:\\alpha \\xrightarrow{\\,o\\} \\beta\\ ,\\forall s\\subseteq \\alpha\\,\\big(\\operatorname{OrdConnected}(s) \\Rightarrow \\operatorname{OrdConnected}(e''s)\\big)$$$
Lean4
@[instance]
theorem ordConnected_image {E : Type*} [EquivLike E α β] [OrderIsoClass E α β] (e : E) {s : Set α}
[hs : OrdConnected s] : OrdConnected (e '' s) :=
by
erw [(e : α ≃o β).image_eq_preimage]
apply ordConnected_preimage (e : α ≃o β).symm
