English
If for every y ∈ K, eventually near (x0,y) P holds, then eventually near x0 we have ∀ y ∈ K, P(x,y).
Русский
Если для каждого y ∈ K выполняются свойства P(x,y) мгновенно (в окрестности (x0,y)), то существует окрестность x0, в которой выполняется ∀ y ∈ K, P(x,y).
LaTeX
$$$\\Big(\\forall y \\in K, \\; P_y \\text{ Eventually near } (x_0,y)\\Big) \\Rightarrow \\Big(\\exists x \\text{ near } x_0, \\; \\forall y \\in K, \\; P(x,y)\\Big)$$$
Lean4
/-- To show that `∀ y ∈ K, P x y` holds for `x` close enough to `x₀` when `K` is compact,
it is sufficient to show that for all `y₀ ∈ K` there `P x y` holds for `(x, y)` close enough
to `(x₀, y₀)`.
Provided for backwards compatibility,
see `IsCompact.mem_prod_nhdsSet_of_forall` for a stronger statement.
-/
theorem eventually_forall_of_forall_eventually {x₀ : X} {K : Set Y} (hK : IsCompact K) {P : X → Y → Prop}
(hP : ∀ y ∈ K, ∀ᶠ z : X × Y in 𝓝 (x₀, y), P z.1 z.2) : ∀ᶠ x in 𝓝 x₀, ∀ y ∈ K, P x y :=
by
simp only [nhds_prod_eq, ← eventually_iSup, ← hK.prod_nhdsSet_eq_biSup] at hP
exact hP.curry.mono fun _ h ↦ h.self_of_nhdsSet
