continuousAt_prod_of_discrete_right

English

If β is discrete, ContinuousAt f x is equivalent to ContinuousAt (b ↦ f(x1, b)) at x2.

Русский

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

LaTeX

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

Lean4

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

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