isClosed_image_coe — Mathlib

English

The image of a set under the embedding is closed iff the original set is closed and compact.

Русский

Образ множества под вложением замкнут тогда и только тогда, когда множество замкнуто и компактно.

LaTeX

$$$IsClosed(\\iota''s) \\iff IsClosed(s) \\land IsCompact(s).$$$

Lean4

@[simp]
theorem isClosed_image_coe {s : Set X} : IsClosed ((↑) '' s : Set (OnePoint X)) ↔ IsClosed s ∧ IsCompact s := by
  rw [← isOpen_compl_iff, isOpen_compl_image_coe]

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