ωScottContinuous_iff_apply₂ — Mathlib

English

A function f is ωScottContinuous iff all its coordinate maps f · a are ωScottContinuous for every a.

Русский

Функция f ωScott непрерывна тогда и только тогда, когда все её координатные отображения f · a являются ωScott непрерывными для каждого a.

LaTeX

$$$\omegaScottContinuous f \iff \forall a, \omegaScottContinuous (f \cdot a)$$$

Lean4

theorem ωScottContinuous_iff_apply₂ : ωScottContinuous f ↔ ∀ a, ωScottContinuous (f · a) :=
  ⟨ωScottContinuous.apply₂, ωScottContinuous.of_apply₂⟩

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