continuousOn_prod_of_discrete_left

English

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

Русский

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

LaTeX

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

Lean4

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

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