continuousOn_prod_of_discrete_right

English

Let β be discrete. A function f: α × β → γ is ContinuousOn on s iff for every b ∈ β the function a ↦ f(a,b) is ContinuousOn on {a : (a,b) ∈ s}.

Русский

Пусть β дискретно. Функция f: α × β → γ непрерывна на s тогда и только тогда, когда для каждого b ∈ β функция a ↦ f(a,b) непрерывна на {a : (a,b) ∈ s}.

LaTeX

$$$$\text{ContinuousOn } f\ s \iff \forall b,\ \text{ContinuousOn }\bigl( a \mapsto f(a,b) \bigr)\bigl\{ a \mid (a,b) \in s \bigr\}. $$$$

Lean4

theorem continuousOn_prod_of_discrete_right [DiscreteTopology β] {f : α × β → γ} {s : Set (α × β)} :
    ContinuousOn f s ↔ ∀ b, ContinuousOn (f ⟨·, b⟩) {a | (a, b) ∈ s} := by
  simp_rw [ContinuousOn, Prod.forall, continuousWithinAt_prod_of_discrete_right]; apply forall_swap

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