formalize some basics in topology with sorries

Author: daniel-levin

Minimathlib/Topology.lean

@@ -26,3 +26,80 @@ theorem isClosed_univ : isClosed (𝒰 : Set X) := by
   unfold isClosed
   rw [@Set.compl_univ]
   exact TopologicalSpace.isOpen_empty
+
+open TopologicalSpace
+
+-- De Morgan's laws for closed sets
+theorem isClosed_iUnion : ∀ {ι : Type u} (s : ι → Set X), (∀ i, isClosed (s i)) → isClosed (⋃ s) := by
+  sorry
+
+theorem isClosed_union : ∀ s t : Set X, isClosed s → isClosed t → isClosed (s ∪ t) := by
+  sorry
+
+-- Basic subset relation
+def subset (s t : Set X) : Prop := ∀ x, x ∈ s → x ∈ t
+
+infixl:50 " ⊆ " => subset
+
+-- Neighborhood definitions and properties
+def nhds (x : X) : Set (Set X) := fun s => ∃ t, isOpen t ∧ x ∈ t ∧ t ⊆ s
+
+theorem isOpen_iff_nhds : ∀ s : Set X, isOpen s ↔ ∀ x, x ∈ s → s ∈ nhds x := by
+  sorry
+
+-- Closure (intersection of all closed supersets)
+def closure (s : Set X) : Set X := fun x => ∀ t, isClosed t → s ⊆ t → x ∈ t
+
+-- Interior (union of all open subsets)
+def interior (s : Set X) : Set X := fun x => ∃ t, isOpen t ∧ t ⊆ s ∧ x ∈ t
+
+theorem closure_closed : ∀ s : Set X, isClosed (closure s) := by
+  sorry
+
+theorem interior_open : ∀ s : Set X, isOpen (interior s) := by
+  sorry
+
+theorem subset_closure : ∀ s : Set X, s ⊆ closure s := by
+  sorry
+
+theorem interior_subset : ∀ s : Set X, interior s ⊆ s := by
+  sorry
+
+-- Dense sets
+def dense (s : Set X) : Prop := closure s = 𝒰
+
+theorem dense_iff_closure : ∀ s : Set X, dense s ↔ closure s = 𝒰 := by
+  sorry
+
+-- Preimage of a function
+def preimage {Y : Type u} (f : X → Y) (s : Set Y) : Set X := fun x => s (f x)
+
+-- Continuity
+def continuous {Y : Type u} [TopologicalSpace Y] (f : X → Y) : Prop :=
+  ∀ s : Set Y, @TopologicalSpace.isOpen Y _ s → isOpen (preimage f s)
+
+theorem continuous_comp {Y Z : Type u} [TopologicalSpace Y] [TopologicalSpace Z]
+  (f : X → Y) (g : Y → Z) : continuous f → continuous g → continuous (fun x => g (f x)) := by
+  sorry
+
+-- Homeomorphisms
+def homeomorphism {Y : Type u} [TopologicalSpace Y] (f : X → Y) : Prop :=
+  continuous f ∧ ∃ g : Y → X, continuous g ∧ (∀ y, f (g y) = y) ∧ (∀ x, g (f x) = x)
+
+theorem homeomorphism_equiv {Y : Type u} [TopologicalSpace Y]
+  (f : X → Y) : homeomorphism f ↔ continuous f ∧ ∃ g : Y → X, continuous g ∧ (∀ y, f (g y) = y) ∧ (∀ x, g (f x) = x) := by
+  sorry
+
+-- Nonempty predicate for sets
+def nonempty (s : Set X) : Prop := ∃ x, x ∈ s
+
+-- Connectedness
+def connected (s : Set X) : Prop :=
+  ¬∃ u v : Set X, isOpen u ∧ isOpen v ∧ u ∩ v = ∅ ∧ s ⊆ u ∪ v ∧ nonempty (fun x => s x ∧ u x) ∧ nonempty (fun x => s x ∧ v x)
+
+-- Image of a function
+def image {Y : Type u} (f : X → Y) (s : Set X) : Set Y := fun y => ∃ x, s x ∧ f x = y
+
+theorem connected_intermediate_value {Y : Type u} [TopologicalSpace Y]
+  (f : X → Y) (s : Set X) : connected s → continuous f → connected (image f s) := by
+  sorry