of_apply₂ — Mathlib

English

If for every a, the function x ↦ f x a is ωScottContinuous, then f is ωScottContinuous.

Русский

Если для каждого a функция x ↦ f x a является ωScott непрерывной, то f тоже ωScott непрерывна.

LaTeX

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

Lean4

theorem of_apply₂ (hf : ∀ a, ωScottContinuous (f · a)) : ωScottContinuous f :=
  ωScottContinuous.of_monotone_map_ωSup ⟨fun _ _ h a ↦ (hf a).monotone h, fun c ↦ by ext a; apply (hf a).map_ωSup c⟩

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