長めの例: コンパクト集合の連続像

コンパクト集合の連続像はコンパクトです． さらに，値域が Hausdorff 空間ならコンパクト集合は閉集合です． したがって，Hausdorff 空間への連続写像では，コンパクト集合の像は閉集合になります．

section CompactImage

variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y]
variable {s : Set X} {f : X → Y}

example (hs : IsCompact s) (hf : Continuous f) : IsClosed (f '' s) := by
  exact (hs.image hf).isClosed

end CompactImage

ここで [T2Space Y] は，Y が Hausdorff 空間であるという型クラス仮定です． 定理 IsCompact.isClosed は一般の位相空間では成り立たず，Hausdorff 条件を要求します． 型クラス仮定として必要な位相的条件が明示されるのは，Mathlib の位相の読み方で重要です．