isClosed_preimage_ofLawson — Mathlib

English

The preimage of a set under the isomorphism toLawson is closed in the Lawson topology if and only if the set is closed in the Lawson topology on α.

Русский

Образ предобраза по изоморфизму toLawson является Lawson-замкнутым тогда и только тогда, когда множество замкнуто в Lawson topology на α.

LaTeX

$$$IsClosed (\mathrm{preimage}(\mathrm{toLawson}, S)) \iff IsClosed_{lawson(\alpha)}(S)$$$

Lean4

theorem isClosed_preimage_ofLawson {S : Set α} : IsClosed (ofLawson ⁻¹' S) ↔ IsClosed[lawson α] S :=
  Iff.rfl

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