English
If s is OrdConnected and f is antitone 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 antitone on a set `t`,
when intersected with `t`, is `OrdConnected`. More precisely, it is the intersection with `t`
of an `OrdConnected` set. -/
theorem preimage_antitoneOn {f : β → α} {t : Set β} {s : Set α} (hs : OrdConnected s) (hf : AntitoneOn f t) :
∃ u, OrdConnected u ∧ t ∩ f ⁻¹' s = t ∩ u :=
(OrdConnected.preimage_monotoneOn hs.dual hf.dual_right :)
