Define metric-related structures

Author: nguyenvukhang

.github/workflows/ci.yml

@@ -0,0 +1,25 @@
+name: CI
+
+on:
+  push:
+    branches:
+      - main
+      - dev
+    tags:
+      - "v[0-9]+.[0-9]+.[0-9]+"
+
+permissions:
+  contents: write
+
+jobs:
+  lean:
+    runs-on: ubuntu-24.04
+    steps:
+      - run: cargo install --git https://github.com/nguyenvukhang/slope.git
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1
+        with:
+          build: false
+          lint: false
+          test: false
+      - run: make all

.github/workflows/create-release.yml

@@ -1,3 +1,7 @@
+import Munkres.Defs.Basic
+import Munkres.Defs.Compact
+import Munkres.Defs.Conversions
 import Munkres.Defs.IsBasisAt
-import Munkres.Defs.Neighborhood
+import Munkres.Defs.Metric.Basic
+import Munkres.Defs.OpenCover
 -- WARNING: THIS FILE IS AUTO-GENERATED.

.github/workflows/lean_action_ci.yml

@@ -6,22 +6,13 @@ import Munkres.Defs.Basic
 
 namespace Munkres
 
--- import Dino.Core.Topology.IsCountableBasisAt
--- import Dino.Core.Set.Subcollection
-
-open Topology Filter ENNReal NNReal TopologicalSpace
+open Topology Filter NNReal
 
 universe u
 
-variable {α : Type u}
-
--- Equivalence of the idea of convergence. WOH.
-example [TopologicalSpace α] (f : ℕ → α) (x : α)
-  : Tendsto f atTop (𝓝 x) ↔ ∀ U, x ∈ U → IsOpen U → ∃ N, ∀ k ≥ N, f k ∈ U
-  := by --
-  rw [tendsto_atTop_nhds] -- ∎
+variable {α : Type u} [MetricSpace α] {X : Set α}
 
-theorem Metric.isComplete_iff [MetricSpace α] {X : Set α}
+protected theorem Metric.isComplete_iff
   : IsComplete X ↔ ∀ (f : ℕ → X), CauchySeq f → ∃ x, Tendsto f atTop (𝓝 x)
   := by --
   constructor
@@ -33,59 +24,45 @@ theorem Metric.isComplete_iff [MetricSpace α] {X : Set α}
     rw [<-completeSpace_coe_iff_isComplete]
     exact UniformSpace.complete_of_cauchySeq_tendsto h -- ∎
 
--- theorem Metric.isCompleteSpace_iff [MetricSpace α]
---   : CompleteSpace α ↔ ∀ (f : ℕ → α), CauchySeq f → ∃ x, Tendsto f atTop (𝓝 x)
---   := by --
---   rw [completeSpace_iff_isComplete_univ, Metric.isComplete_iff]
---   constructor
---   · intro h f hf
---     let X : Set α := Set.univ; let φ : X ≃ α := Equiv.Set.univ α
---     let f' : ℕ → X := (φ.invFun <| f ·)
---     have hf' : CauchySeq f' := by
---       rw [cauchySeq_iff'] at hf ⊢
---       exact hf
---     obtain ⟨x, hx⟩ := h f' hf'
---     use x
---     rw [tendsto_atTop] at hx ⊢
---     exact hx
---   · intro h f' hf'
---     let X : Set α := Set.univ; let φ : X ≃ α := Equiv.Set.univ α
---     let f : ℕ → α := φ ∘ f'
---     have hf : CauchySeq f := by rw [cauchySeq_iff'] at hf' ⊢; exact hf'
---     obtain ⟨x, hx⟩ := h f hf
---     use ⟨x, trivial⟩
---     exact tendsto_subtype_rng.mpr hx -- ∎
+protected theorem Metric.CompleteSpace_iff
+  : CompleteSpace α ↔ ∀ (f : ℕ → α), CauchySeq f → ∃ x, Tendsto f atTop (𝓝 x)
+  := by --
+  rw [completeSpace_iff_isComplete_univ, Metric.isComplete_iff]
+  simp only [Metric.cauchySeq_iff', tendsto_subtype_rng]
+  simp only [Subtype.exists, Set.mem_univ, exists_const]
+  let φ := Equiv.Set.univ α
+  -- exact ⟨fun h f ↦ h (φ.symm ∘ f), fun h f' ↦ h (φ ∘ f')⟩
+  exact ⟨(· <| φ.symm ∘ ·), (· <| φ ∘ ·)⟩ -- ∎
+
+-- Equivalence for the idea of total boundedness.
+example : TotallyBounded X ↔ ∀ ε > 0, ∃ t : Set α, t.Finite ∧ X ⊆ ⋃ y ∈ t, Metric.ball y ε
+  := by --
+  exact Metric.totallyBounded_iff -- ∎
 
 section LebesgueNumber
 
 universe v
-variable [MetricSpace α] {ι : Sort v} {c : ι → Set α} {U : Set (Set α)}
+variable {ι : Sort v} {c : ι → Set α} {δ : ℝ≥0}
+  {U : Set (Set α)} {ho : ∀ i, IsOpen (c i)} {hc : Set.univ ⊆ ⋃ i, c i}
 
 /-- Tells us if `δ` is a lebesgue number of the open cover `c`. -/
 class LebesgueNumber (δ : ℝ≥0) (ho : ∀ i, IsOpen (c i)) (hc : Set.univ ⊆ ⋃ i, c i) : Prop where
   ne_zero : δ ≠ 0
   out : ∀ s : Set α, EMetric.diam s < δ → ∃ i, s ⊆ c i
 
-lemma LebesgueNumber.pos {δ : ℝ≥0} {ho : ∀ i, IsOpen (c i)} {hc : Set.univ ⊆ ⋃ i, c i}
-  (h : LebesgueNumber δ ho hc) : δ > 0 := pos_of_ne_zero h.ne_zero
+lemma LebesgueNumber.pos (h : LebesgueNumber δ ho hc) : δ > 0 := pos_of_ne_zero h.ne_zero
 
-protected theorem LebesgueNumber.iff {δ : ℝ≥0} {ho : ∀ i, IsOpen (c i)} {hc : Set.univ ⊆ ⋃ i, c i}
-  : LebesgueNumber δ ho hc ↔ δ > 0 ∧ ∀ s : Set α, EMetric.diam s < δ → ∃ i, s ⊆ c i
+protected theorem LebesgueNumber.iff : LebesgueNumber δ ho hc
+  ↔ δ ≠ 0 ∧ ∀ s : Set α, EMetric.diam s < δ → ∃ i, s ⊆ c i
   := by --
   constructor
   · intro h
-    exact ⟨h.pos, h.out⟩
-  · intro ⟨pos, out⟩
-    exact {ne_zero := pos.ne', out} -- ∎
+    exact ⟨h.ne_zero, h.out⟩
+  · intro ⟨ne_zero, out⟩
+    exact {ne_zero, out} -- ∎
 
 -- For more info in Mathlib, look for `lebesgue_number_lemma_of_emetric`.
 
 end LebesgueNumber
 
--- Equivalence for the idea of total boundedness.
-example [MetricSpace α] {X : Set α} :
-  TotallyBounded X ↔ ∀ ε > 0, ∃ t : Set α, t.Finite ∧ X ⊆ ⋃ y ∈ t, Metric.ball y ε
-  := by --
-  exact Metric.totallyBounded_iff -- ∎
-
 end Munkres

.github/workflows/update.yml

@@ -0,0 +1,38 @@
+-- A bit of a failed experiment with open covers. Maybe we're better off just
+-- using regular sets instead of trying to define structs.
+import Mathlib.Data.SetLike.Basic
+import Mathlib.Topology.Defs.Basic
+
+namespace Munkres
+
+universe u w
+
+variable
+  {α : Type u} [TopologicalSpace α]
+  {ι : Type w}
+
+@[ext]
+structure iOpenCover (K : Set α) (ι : Type w) where
+  toFun : ι → Set α
+  isOpen' : ∀ i, IsOpen (toFun i)
+  cover' : K ⊆ ⋃ i, toFun i
+
+instance (K : Set α) : FunLike (iOpenCover K ι) ι (Set α) where
+  coe := iOpenCover.toFun
+  coe_injective' _ _ := iOpenCover.ext
+
+@[ext]
+structure sOpenCover (K : Set α) where
+  carrier : Set (Set α)
+  isOpen' : ∀ u ∈ carrier, IsOpen u
+  cover' : K ⊆ ⋃₀ carrier
+
+instance (K : Set α) : SetLike (sOpenCover K) (Set α) where
+  coe := sOpenCover.carrier
+  coe_injective' _ _ := sOpenCover.ext
+
+-- example {K : Set α} : IsCompact K ↔ ∀ {ι : Type*} (U : iOpenCover K ι),
+-- ∃ F : iOpenCover K ι, F := by
+--   sorry
+
+end Munkres