continuous — Mathlib

English

Continuity of seq composition: continuous F yields F after seq maps being ωScottContinuous.

Русский

Непрерывность последовательного композиционного отображения: непрерывность F после seq-мэппинга.

LaTeX

$$continuous (F) (C) : F (ωSup C) = ωSup (C.map F)$$

Lean4

theorem continuous (F : α →𝒄 β) (C : Chain α) : F (ωSup C) = ωSup (C.map F) :=
  F.ωScottContinuous.map_ωSup _

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