Define metric-related structures

Author: nguyenvukhang

Munkres/Defs.lean

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

Munkres/Defs/Metric/Basic.lean

@@ -6,16 +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} [MetricSpace α]
+variable {α : Type u} [MetricSpace α] {X : Set α}
 
-theorem Metric.isComplete_iff {X : Set α}
+protected theorem Metric.isComplete_iff
   : IsComplete X ↔ ∀ (f : ℕ → X), CauchySeq f → ∃ x, Tendsto f atTop (𝓝 x)
   := by --
   constructor
@@ -27,59 +24,45 @@ theorem Metric.isComplete_iff {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 {ι : 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