lawsonClosed_of_lowerClosed — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem lawsonClosed_of_lowerClosed (s : Set α) (h : IsClosed (WithLower.ofLower ⁻¹' s)) :
    IsClosed (WithLawson.ofLawson ⁻¹' s) :=
  h.mono lawson_le_lower

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