apply₂ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem apply₂ (hf : ωScottContinuous f) (a : α) : ωScottContinuous (f · a) :=
  ωScottContinuous.of_monotone_map_ωSup ⟨fun _ _ h ↦ hf.monotone h a, fun c ↦ congr_fun (hf.map_ωSup c) a⟩

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