continuousAt_prod_of_discrete_left

English

If α is discrete, then ContinuousAt f x for f: α × β → γ is equivalent to ContinuousAt (a ↦ f(a, x2)) at a = x1.

Русский

Если α дискретно, то ContinuousAt f x эквивалентно ContinuousAt (a ↦ f(a, x2)) в точке a = x1.

LaTeX

$$$$\text{ContinuousAt } f\,(x_1,x_2) \iff \text{ContinuousAt }\bigl(a \mapsto f(a, x_2)\bigr)\!\bigl(x_1\bigr).$$$$

Lean4

theorem continuousAt_prod_of_discrete_left [DiscreteTopology α] {f : α × β → γ} {x : α × β} :
    ContinuousAt f x ↔ ContinuousAt (f ⟨x.1, ·⟩) x.2 := by simp_rw [← continuousWithinAt_univ];
  exact continuousWithinAt_prod_of_discrete_left

Похожие утверждения