English
Let α be a discrete space. For f: α × β → γ, s ⊆ α × β, and x = (x1, x2), ContinuousWithinAt f s x is equivalent to ContinuousWithinAt (f(·, x2)) on the fiber { a ∈ α : (a, x2) ∈ s } at x1.
Русский
Пусть α — дискретное пространство. Для f: α × β → γ, s ⊆ α × β и x = (x1, x2), ContinuousWithinAt f s x эквивалентно непрерывности функции a ↦ f(a, x2) на волокне { a ∈ α : (a, x2) ∈ s } в точке x1.
LaTeX
$$$$\text{ContinuousWithinAt } f\ s\ x \iff \text{ContinuousWithinAt }\bigl(a \mapsto f(a, x_2)\bigr)\bigl\{ a \in \alpha \mid (a, x_2) \in s \bigr\} x_1.$$$$
Lean4
theorem continuousWithinAt_prod_of_discrete_right [DiscreteTopology β] {f : α × β → γ} {s : Set (α × β)} {x : α × β} :
ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ⟨·, x.2⟩) {a | (a, x.2) ∈ s} x.1 := by rw [← x.eta];
simp_rw [ContinuousWithinAt, nhdsWithin, nhds_prod_eq, nhds_discrete, prod_pure, ← map_inf_principal_preimage]; rfl
