comp — Mathlib

English

If g and f are ωScott-continuous, then their composition g ∘ f is ωScott-continuous.

Русский

Если g и f ω Scott‑непрерывны, то композиция g ∘ f тоже ωScott‑непрерывна.

LaTeX

$$$$ \omegaScottContinuous g \rightarrow \omegaScottContinuous f \rightarrow \omegaScottContinuous (g \circ f). $$$$

Lean4

theorem comp (hg : ωScottContinuous g) (hf : ωScottContinuous f) : ωScottContinuous (g.comp f) :=
  ωScottContinuous.of_monotone_map_ωSup ⟨hg.monotone.comp hf.monotone, by simp [hf.map_ωSup, hg.map_ωSup, map_comp]⟩

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