prodMk — Mathlib

English

If f and g are ωScottContinuous, then x ↦ (f x, g x) is ωScottContinuous.

Русский

Если f и g ωScott непрерывны, то отображение x ↦ (f x, g x) также ωScott непрерывно.

LaTeX

$$$\omegaScottContinuous f \land \omegaScottContinuous g \Rightarrow \omegaScottContinuous (x \mapsto (f x, g x))$$$

Lean4

theorem prodMk (hf : ωScottContinuous f) (hg : ωScottContinuous g) : ωScottContinuous fun x => (f x, g x) :=
  ScottContinuousOn.prodMk (fun a b hab => by use pair a b hab; exact range_pair a b hab) hf hg

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