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