English
If s is OrdConnected and f is monotone on t, then there exists a subset u that is OrdConnected such that t ∩ f^{-1}(s) = t ∩ u.
Русский
Пусть s упорядочно связно, а f монотонна на t; тогда существует подмножество u упорядоченно связное такое, что t ∩ f^{-1}(s) = t ∩ u.
LaTeX
$$$\\exists u\\, (\\operatorname{OrdConnected}(u) \\land t \\cap f^{-1}(s) = t \\cap u)$$$
Lean4
/-- The preimage of an `OrdConnected` set under a map which is monotone on a set `t`,
when intersected with `t`, is `OrdConnected`. More precisely, it is the intersection with `t`
of an `OrdConnected` set. -/
theorem preimage_monotoneOn {f : β → α} {t : Set β} {s : Set α} (hs : OrdConnected s) (hf : MonotoneOn f t) :
∃ u, OrdConnected u ∧ t ∩ f ⁻¹' s = t ∩ u :=
by
let u := {x | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ (∃ z ∈ t, x ≤ z ∧ f z ∈ s)}
refine ⟨u, ⟨?_⟩, Subset.antisymm ?_ ?_⟩
· rintro x ⟨⟨y, yt, yx, ys⟩, -⟩ x' ⟨-, ⟨z, zt, x'z, zs⟩⟩ a ha
exact ⟨⟨y, yt, yx.trans ha.1, ys⟩, ⟨z, zt, ha.2.trans x'z, zs⟩⟩
· rintro x ⟨xt, xs⟩
exact ⟨xt, ⟨x, xt, le_rfl, xs⟩, ⟨x, xt, le_rfl, xs⟩⟩
· rintro x ⟨xt, ⟨y, yt, yx, ys⟩, ⟨z, zt, xz, zs⟩⟩
refine ⟨xt, ?_⟩
apply hs.out ys zs
exact ⟨hf yt xt yx, hf xt zt xz⟩
