update mathlib

dwrensha · Nov 9, 2024 · f86a1ae · f86a1ae
1 parent 3ed2faf
commit f86a1ae
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/Compfiles/UpperLowerContinuous.lean b/Compfiles/UpperLowerContinuous.lean
@@ -127,9 +127,9 @@ lemma lower_basis :
   · intro I1 hI1 I2 hI2 x hx;
     obtain ⟨a, b, hab⟩ := hI1
     obtain ⟨c, d, hcd⟩ := hI2
-    use Set.Ico (Sup.sup a c) (Inf.inf b d)
+    use Set.Ico (max a c) (min b d)
     constructor
-    · exact ⟨Sup.sup a c, Inf.inf b d, rfl ⟩
+    · exact ⟨max a c, min b d, rfl ⟩
     · constructor
       · aesop
       · intro y hy
@@ -149,9 +149,9 @@ lemma upper_basis :
   · intro I1 hI1 I2 hI2 x hx;
     obtain ⟨a, b, hab⟩ := hI1
     obtain ⟨c, d, hcd⟩ := hI2
-    use Set.Ioc (Sup.sup a c) (Inf.inf b d)
+    use Set.Ioc (max a c) (min b d)
     constructor
-    · exact ⟨Sup.sup a c, Inf.inf b d, rfl⟩
+    · exact ⟨max a c, min b d, rfl⟩
     · constructor
       · aesop
       · intro y hy
@@ -171,9 +171,9 @@ lemma open_basis :
  · intro I1 hI1 I2 hI2 x hx
    obtain ⟨a, b, hab⟩ := hI1
    obtain ⟨c, d, hcd⟩ := hI2
-   use Set.Ioo (Sup.sup a c) (Inf.inf b d)
+   use Set.Ioo (max a c) (min b d)
    constructor
-   · exact ⟨Sup.sup a c, Inf.inf b d, rfl⟩
+   · exact ⟨max a c, min b d, rfl⟩
    · constructor
      · aesop
      · intro y hy; aesop

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2b878991c9059cada386578e7da9a601b249102e",
+   "rev": "5476cef777111bb7a13cd11b7ba78b24fdb2d04f",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",