Add subtype lemmas

Author: nguyenvukhang

Munkres/Defs.lean

@@ -4,4 +4,6 @@ import Munkres.Defs.Conversions
 import Munkres.Defs.IsBasisAt
 import Munkres.Defs.Metric.Basic
 import Munkres.Defs.OpenCover
+import Munkres.Defs.Subspace
+import Munkres.Defs.Subtype
 -- WARNING: THIS FILE IS AUTO-GENERATED.

Munkres/Defs/Subspace.lean

@@ -0,0 +1,33 @@
+import Munkres.Subtype.Induced
+
+import Munkres.Defs.Subtype
+
+open Set
+
+universe u
+
+variable {α : Type u} {X Y : Set α} [tY : TopologicalSpace Y]
+
+def Topology.Subspace (h : X ⊆ Y) : TopologicalSpace X
+  := by --
+  let X' := { y : Y | ↑y ∈ X }
+  let φ : X ≃ X' := {
+    toFun := fun ⟨x, hx⟩ ↦ ⟨⟨x, h hx⟩, hx⟩
+    invFun := fun ⟨⟨x, _⟩, hx⟩ ↦ ⟨x, hx⟩
+    left_inv := Function.leftInverse_iff_comp.mpr rfl
+    right_inv := Function.rightInverse_iff_comp.mpr rfl
+  }
+  let tX : TopologicalSpace X' := instTopologicalSpaceSubtype (p := fun x : Y ↦ ↑x ∈ X)
+  refine {
+    IsOpen U := IsOpen (φ '' U)
+    isOpen_univ := by
+      rw [image_univ, EquivLike.range_eq_univ]
+      exact isOpen_univ
+    isOpen_inter s t hs ht := by
+      rw [image_inter φ.injective]
+      exact hs.inter ht
+    isOpen_sUnion s hs := by
+      rw [sUnion_eq_biUnion]
+      rw [image_iUnion₂]
+      exact isOpen_biUnion hs
+  } -- ∎

Munkres/Defs/Subtype.lean

@@ -0,0 +1,24 @@
+import Mathlib.Topology.Separation.Hausdorff
+
+namespace Munkres
+
+universe u
+
+variable {α : Type u}
+
+-- Conforms to Munkres' idea of a set being open in a subspace.
+structure IsOpenIn (A X : Set α) [TopologicalSpace X] : Prop where
+  isOpen' : @IsOpen X _ (Subtype.val ⁻¹' A)
+  subset' : A ⊆ X
+
+-- Conforms to Munkres' idea of a set being closed in a subspace.
+structure IsClosedIn (A X : Set α) [TopologicalSpace X] : Prop where
+  isClosed' : @IsClosed X _ (Subtype.val ⁻¹' A)
+  subset' : A ⊆ X
+
+-- Conforms to Munkres' idea of a set being compact in a subspace.
+structure IsCompactIn (A X : Set α) [TopologicalSpace X] : Prop where
+  isCompact' : @IsCompact X _ (Subtype.val ⁻¹' A)
+  subset' : A ⊆ X
+
+end Munkres

Munkres/Mathlib/Subtype.lean

@@ -0,0 +1,65 @@
+import Mathlib.Data.Set.Image
+import Mathlib.Data.Set.Notation
+
+universe u
+
+variable {α : Type u}
+
+section Examples
+open Subtype
+variable {X U : Set α}
+
+/-- Reminder of other forms that `Subtype.val ⁻¹' U` might take! -/
+example : Subtype.val⁻¹' U = { x : X | ↑x ∈ U } := rfl
+example : (↑) '' ((↑) ⁻¹' U : Set X) = X ∩ U := image_preimage_val X U
+example : (↑) '' ((↑) ⁻¹' U : Set X) = X ∩ U := image_preimage_coe X U
+example : val '' (val ⁻¹' U : Set X) = X ∩ U := image_preimage_val X U
+example : val '' (val ⁻¹' U : Set X) = X ∩ U := image_preimage_coe X U
+
+example (h : U ⊆ X) : val '' { x : X | ↑x ∈ U } = U := coe_image_of_subset h
+
+end Examples
+
+section Lemmas
+variable {X U : Set α}
+
+theorem Subtype.preimage_val_eq_iff (A : Set X)
+  : val ⁻¹' U = A ↔ val '' A = X ∩ U
+  := by --
+  constructor
+  · intro h
+    subst h
+    exact image_preimage_val X U
+  · intro h
+    rw [<-preimage_coe_self_inter, <-h, Set.preimage_image_eq]
+    exact val_injective -- ∎
+
+theorem Subtype.preimage_coe_eq_iff (A : Set X)
+  : (↑) ⁻¹' U = A ↔ (↑) '' A = X ∩ U
+  := by --
+  exact preimage_val_eq_iff A -- ∎
+
+theorem Subtype.eq_inter : { x : X | ↑x ∈ U } = X ∩ U
+  := by --
+  exact (preimage_val_eq_iff _).mp rfl -- ∎
+
+theorem Subtype.mem_iff (A : Set X) (x : X) : x ∈ A ↔ x.val ∈ (↑) '' A
+  := by --
+  refine ⟨(⟨x, ·, rfl⟩), ?_⟩
+  intro ⟨y, hy, heq⟩
+  rw [SetCoe.ext heq] at hy
+  exact hy -- ∎
+
+theorem Subtype.set_eq (A : Set X) : { x : X | ↑x ∈ (A : Set α) } = A
+  := by --
+  refine le_antisymm ?_ (⟨·, ·, rfl⟩)
+  intro x ⟨y, hy, heq⟩
+  rw [SetCoe.ext heq] at hy
+  exact hy -- ∎
+
+theorem Subtype.compl : (val ⁻¹' U : Set X)ᶜ = val ⁻¹' (X \ U)
+  := by --
+  rw [Set.preimage_diff, coe_preimage_self]
+  exact Set.compl_eq_univ_diff (val ⁻¹' U) -- ∎
+
+end Lemmas

Munkres/Subtype/Induced.lean

@@ -0,0 +1,37 @@
+import Mathlib.Topology.Order
+
+import Munkres.Mathlib.Subtype
+
+universe u
+
+variable {α : Type u} [TopologicalSpace α]
+
+section Induced
+
+variable (X : Set α) {A : Set α}
+
+/-- Matches Munkres' definition of a set being open in a topological subspace. -/
+theorem isOpen_induced_iff₂ (A : Set X) : @IsOpen X _ A ↔ ∃ U, IsOpen U ∧ A = X ∩ U
+  := by --
+  rw [isOpen_induced_iff]
+  simp only [Subtype.preimage_val_eq_iff] -- ∎
+
+/-- Matches Munkres' definition of a set being closed in a topological subspace. -/
+theorem isClosed_induced_iff₂ (A : Set X) : @IsClosed X _ A ↔ ∃ U, IsClosed U ∧ A = X ∩ U
+  := by --
+  rw [isClosed_induced_iff]
+  simp only [Subtype.preimage_val_eq_iff] -- ∎
+
+theorem isOpen_induced_iff₃ :
+  @IsOpen X _ (Subtype.val ⁻¹' A) ↔ ∃ U, IsOpen U ∧ X ∩ A = X ∩ U
+  := by --
+  rw [isOpen_induced_iff]
+  simp only [Subtype.preimage_val_eq_iff, Subtype.image_preimage_coe] -- ∎
+
+theorem isClosed_induced_iff₃ :
+  @IsClosed X _ (Subtype.val ⁻¹' A) ↔ ∃ U, IsClosed U ∧ X ∩ A = X ∩ U
+  := by --
+  rw [isClosed_induced_iff]
+  simp only [Subtype.preimage_val_eq_iff, Subtype.image_preimage_coe] -- ∎
+
+end Induced

Munkres/Subtype/Topology.lean

@@ -0,0 +1,115 @@
+import Munkres.Subtype.Induced
+
+import Munkres.Defs.Subtype
+
+open Set
+
+namespace Munkres
+
+universe u
+
+variable {α : Type u}
+
+section SimpleCases
+variable {X A : Set α} [TopologicalSpace X]
+
+-- Empty and univ lemmas.
+
+lemma isOpenIn_empty : IsOpenIn ∅ X
+  := by --
+  exact { isOpen' := isOpen_const, subset' := empty_subset X } -- ∎
+lemma isOpenIn_univ : IsOpenIn X X
+  := by --
+  refine { isOpen' := ?_, subset' := le_rfl }
+  rw [Subtype.coe_preimage_self]
+  exact isOpen_univ -- ∎
+
+lemma isClosedIn_empty : IsClosedIn ∅ X
+  := by --
+  exact { isClosed' := isClosed_const, subset' := empty_subset X } -- ∎
+lemma isClosedIn_univ : IsClosedIn X X
+  := by --
+  refine { isClosed' := ?_, subset' := le_rfl }
+  rw [Subtype.coe_preimage_self]
+  exact isClosed_univ -- ∎
+
+lemma isCompactIn_empty : IsCompactIn ∅ X
+  := by --
+  refine { isCompact' := ?_, subset' := empty_subset X }
+  rw [preimage_empty]
+  exact isCompact_empty -- ∎
+
+-- Complement lemmas.
+
+lemma IsClosedIn.isOpen_compl (h : IsClosedIn A X) : IsOpenIn (X \ A) X
+  := by --
+  refine { isOpen' := ?_, subset' := diff_subset }
+  rw [<-Subtype.compl]
+  exact h.isClosed'.isOpen_compl -- ∎
+lemma IsOpenIn.isClosed_compl (h : IsOpenIn A X) : IsClosedIn (X \ A) X
+  := by --
+  refine { isClosed' := ?_, subset' := diff_subset }
+  rw [<-Subtype.compl]
+  exact h.isOpen'.isClosed_compl -- ∎
+
+lemma IsClosedIn.iff_compl : IsClosedIn A X ↔ IsOpenIn (X \ A) X ∧ A ⊆ X
+  := by --
+  refine ⟨fun h ↦ ⟨h.isOpen_compl, h.subset'⟩, ?_⟩
+  intro ⟨h, subset'⟩
+  rw [<-Set.diff_diff_cancel_left subset']
+  exact h.isClosed_compl -- ∎
+lemma IsOpenIn.iff_compl : IsOpenIn A X ↔ IsClosedIn (X \ A) X ∧ A ⊆ X
+  := by --
+  refine ⟨fun h ↦ ⟨h.isClosed_compl, h.subset'⟩, ?_⟩
+  intro ⟨h, subset'⟩
+  rw [<-Set.diff_diff_cancel_left subset']
+  exact h.isOpen_compl -- ∎
+
+end SimpleCases
+
+example [TopologicalSpace α] {A X : Set α}
+  : IsOpenIn A X → IsOpen X → IsOpen A
+  := by
+  intro hAX hX
+  have hA := hAX.isOpen'
+  rw [isOpen_induced_iff₂] at hA
+  obtain ⟨U, hU, hA⟩ := hA
+  rw [Subtype.image_preimage_val] at hA
+  -- have : X ∩ A = A := inter_eq_self_of_subset_right hAX.subset'
+  rw [inter_eq_self_of_subset_right hAX.subset'] at hA
+  subst hA
+  refine hX.inter hU
+
+section IsOpenIn
+variable {X Y A : Set α}
+
+theorem IsOpenIn.lift [TopologicalSpace α]
+  : IsOpenIn A X → IsOpen X → IsOpen A
+  := by --
+  intro hAX hX
+  have hA := hAX.isOpen'
+  rw [isOpen_induced_iff₂] at hA
+  obtain ⟨U, hU, hA⟩ := hA
+  rw [Subtype.image_preimage_val] at hA
+  rw [inter_eq_self_of_subset_right hAX.subset'] at hA
+  subst hA
+  exact hX.inter hU -- ∎
+
+end IsOpenIn
+section IsClosedIn
+variable {X Y A : Set α}
+
+theorem IsClosedIn.lift [TopologicalSpace α]
+  : IsClosedIn A X → IsClosed X → IsClosed A
+  := by --
+  intro hAX hX
+  have hA := hAX.isClosed'
+  rw [isClosed_induced_iff₂] at hA
+  obtain ⟨U, hU, hA⟩ := hA
+  rw [Subtype.image_preimage_val] at hA
+  rw [inter_eq_self_of_subset_right hAX.subset'] at hA
+  subst hA
+  exact hX.inter hU -- ∎
+
+end IsClosedIn
+end Munkres

README.md

@@ -1,13 +1,4 @@
-# topology
+# Munkres
 
-## GitHub configuration
-
-To set up your new GitHub repository, follow these steps:
-
-* Under your repository name, click **Settings**.
-* In the **Actions** section of the sidebar, click "General".
-* Check the box **Allow GitHub Actions to create and approve pull requests**.
-* Click the **Pages** section of the settings sidebar.
-* In the **Source** dropdown menu, select "GitHub Actions".
-
-After following the steps above, you can remove this section from the README file.
+Note: the import order goes: `import`, `open`, `namespace`, `universe`,
+`variable`.

lakefile.toml

@@ -5,7 +5,7 @@ defaultTargets = ["Munkres"]
 
 [leanOptions]
 pp.unicode.fun = true # pretty-prints `fun a ↦ b`
-relaxedAutoImplicit = false
+autoImplicit = false
 weak.linter.mathlibStandardSet = true
 maxSynthPendingDepth = 3