lawsonClosed_of_scottClosed — Mathlib

English

If s is closed in the Scott topology, then its Lawson preimage is closed in WithLawson α.

Русский

Если s замкнуто в топологии Scott, то его предобраз Lawson замкнут в WithLawson α.

LaTeX

$$$(s: Set\ alpha)\; (h: IsClosed(WithScott.ofScott^{-1}' s)) \rightarrow IsClosed(WithLawson.ofLawson^{-1}' s)$$$

Lean4

theorem lawsonClosed_of_scottClosed (s : Set α) (h : IsClosed (WithScott.ofScott ⁻¹' s)) :
    IsClosed (WithLawson.ofLawson ⁻¹' s) :=
  h.mono lawson_le_scott

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