ωScottContinuous_iff_monotone_map_ωSup

English

An ωScott-continuous function f is characterized by existence of a monotone part plus a map-ωSup property, and conversely.

Русский

Функция ωScott-постоянна эквивалентно существованию монотонного отображения и свойству сохранения ωSup; и наоборот.

LaTeX

$$$$ \omegaScottContinuous f \iff \exists hf : \text{Monotone } f, \forall c : \text{Chain } \alpha, f(\omegaSup c) = \omegaSup (c.map (\langle f, hf \rangle)). $$$$

Lean4

/-- `ωScottContinuous f` asserts that `f` is both monotone and distributes over ωSup. -/
theorem ωScottContinuous_iff_monotone_map_ωSup :
    ωScottContinuous f ↔ ∃ hf : Monotone f, ∀ c : Chain α, f (ωSup c) = ωSup (c.map ⟨f, hf⟩) :=
  by
  refine ⟨fun hf ↦ ⟨hf.monotone, hf.map_ωSup⟩, ?_⟩
  intro hf _ ⟨c, hc⟩ _ _ _ hda
  convert isLUB_range_ωSup (c.map { toFun := f, monotone' := hf.1 })
  · rw [map_coe, OrderHom.coe_mk, ← hc, ← (Set.range_comp f ⇑c)]
  · rw [← hc] at hda
    rw [← hf.2 c, ωSup_eq_of_isLUB hda]

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