English
If for every a ∈ s the map x ↦ f(x,a) is continuous and t is closed, then the set {x | MapsTo (f x) s t} is closed.
Русский
Если для каждого a ∈ s отображение x ↦ f(x,a) непрерывно и t замкнуто, то множество {x | MapsTo (f x) s t} замкнуто.
LaTeX
$$IsClosed t → (∀ a ∈ s, Continuous (f · a)) → IsClosed {x | MapsTo (f x) s t}$$
Lean4
/-- If `f x y` is continuous in `x` for all `y ∈ s`,
then the set of `x` such that `f x` maps `s` to `t` is closed. -/
theorem setOf_mapsTo {α : Type*} {f : X → α → Z} {s : Set α} {t : Set Z} (ht : IsClosed t)
(hf : ∀ a ∈ s, Continuous (f · a)) : IsClosed {x | MapsTo (f x) s t} := by
simpa only [MapsTo, setOf_forall] using isClosed_biInter fun y hy ↦ ht.preimage (hf y hy)
