ωScottContinuous_iff_map_ωSup_of_orderHom

English

For any OrderHom f, ωScottContinuous (OrderHom.instFunLike.coe f) is equivalent to preserving ωSup along all chains.

Русский

Для отображения-гомоморфа f эквивалентно сохранение ωSup по всем цепям.

LaTeX

$$$$ \omegaScottContinuous (\text{OrderHom.instFunLike.coe } f) \iff \forall c : \text{Chain } \alpha, f(\omegaSup c) = \omegaSup (c.map f). $$$$

Lean4

theorem ωScottContinuous_iff_map_ωSup_of_orderHom {f : α →o β} :
    ωScottContinuous f ↔ ∀ c : Chain α, f (ωSup c) = ωSup (c.map f) :=
  by
  rw [ωScottContinuous_iff_monotone_map_ωSup]
  exact exists_prop_of_true f.monotone'

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