コンパクト性と連結性

ここまでの IsOpen，IsClosed，Continuous を使って，位相的な性質を扱います． コンパクト性は IsCompact s で表されます． これは s : Set X に対する述語です． 閉集合や連続写像との相互作用は，解析や微分積分で頻繁に使います．

連結性について，Mathlib では空集合も許した連結性を IsPreconnected s と呼びます． 非空性まで含めた通常の連結集合は IsConnected s です． 中間値の定理の証明で本質的に使うのは「2 つの閉集合による分離ができない」という性質なので， IsPreconnected が主役になります．

#check IsCompact
#check IsCompact.image
#check IsClosed
#check IsPreconnected
#check IsConnected
#check isPreconnected_Icc
#check IsPreconnected.intermediate_value
#check intermediate_value_Icc
#check intermediate_value_Icc'

section CompactnessAndConnectedness

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

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

example : IsPreconnected (Icc (0 : ℝ) 1) := by
  exact isPreconnected_Icc

end CompactnessAndConnectedness

IsCompact.image は，コンパクト集合の連続像がコンパクトであることを述べます． isPreconnected_Icc は，閉区間 Icc a b が preconnected であるという定理です． IsPreconnected.intermediate_value は，preconnected な集合上の連続関数について， 端点値の間の閉区間が像に含まれることを述べます． 閉区間に特化した使いやすい形が intermediate_value_Icc です．