coe_scott_continuous — Mathlib

English

The map taking a submodule to its underlying set is ω-Scott continuous.

Русский

Отображение подмодуля в множество непрерывно по ω-цепям.

LaTeX

$$$\text{coe}_{\text{Submodule}\to\text{Set}} : \text{Submodule} \to \text{Set}$ is ω-Scott continuous.$$

Lean4

/-- We can regard `coe_iSup_of_chain` as the statement that `(↑) : (Submodule R M) → Set M` is
Scott continuous for the ω-complete partial order induced by the complete lattice structures. -/
theorem coe_scott_continuous : OmegaCompletePartialOrder.ωScottContinuous ((↑) : Submodule R M → Set M) :=
  OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup ⟨SetLike.coe_mono, coe_iSup_of_chain⟩

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