seq — Mathlib

English

If hf and hg are ωScottContinuous, then the sequential composition x ↦ f x <*> g x is ωScottContinuous.

Русский

Если hf и hg ωScott непрерывны, то секвенциальное композиционное отображение x ↦ f x <*> g x также ωScott непрерывно.

LaTeX

$$$\text{hf}, \text{hg} \Rightarrow \omegaScottContinuous (x \mapsto f x <*> g x)$$$

Lean4

theorem seq {β γ} {f : α → Part (β → γ)} {g : α → Part β} (hf : ωScottContinuous f) (hg : ωScottContinuous g) :
    ωScottContinuous fun x ↦ f x <*> g x := by
  simp only [seq_eq_bind_map]
  exact ωScottContinuous.bind hf <| ωScottContinuous.of_apply₂ fun _ ↦ ωScottContinuous.map hg

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