Bump mathlib

YaelDillies · Sep 27, 2024 · 70db27b · 70db27b
1 parent f8ce814
commit 70db27b
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 11 deletions.
diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean
@@ -23,6 +23,7 @@ import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import LeanCamCombi.Mathlib.Algebra.Module.BigOperators
 import LeanCamCombi.Mathlib.Algebra.Order.BigOperators.LocallyFinite
 import LeanCamCombi.Mathlib.Algebra.Order.Group.Pi
+import LeanCamCombi.Mathlib.Analysis.Convex.Between
 import LeanCamCombi.Mathlib.Analysis.Convex.Exposed
 import LeanCamCombi.Mathlib.Analysis.Convex.Extreme
 import LeanCamCombi.Mathlib.Analysis.Convex.Independence
@@ -48,14 +49,15 @@ import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.Mathlib.GroupTheory.QuotientGroup
 import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.AffineMap
 import LeanCamCombi.Mathlib.Logic.Basic
-import LeanCamCombi.Mathlib.Logic.Function.Defs
 import LeanCamCombi.Mathlib.Order.ConditionallyCompleteLattice.Basic
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition
 import LeanCamCombi.Mathlib.Order.Sublattice
 import LeanCamCombi.Mathlib.Probability.Independence.Basic
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
 import LeanCamCombi.MetricBetween
 import LeanCamCombi.MinkowskiCaratheodory
+import LeanCamCombi.OrderShatter
+import LeanCamCombi.PhD.VCDim.Basic
 import LeanCamCombi.Sight.Sight
 import LeanCamCombi.SimplicialComplex.Basic
 import LeanCamCombi.SimplicialComplex.Finite

diff --git a/LeanCamCombi/ConvexityRefactor/StdSimplex.lean b/LeanCamCombi/ConvexityRefactor/StdSimplex.lean
@@ -7,7 +7,6 @@ import LeanCamCombi.Mathlib.Algebra.BigOperators.Finsupp
 import LeanCamCombi.Mathlib.Algebra.Module.BigOperators
 import LeanCamCombi.Mathlib.Data.Finsupp.Order
 import LeanCamCombi.Mathlib.Logic.Basic
-import LeanCamCombi.Mathlib.Logic.Function.Defs
 
 noncomputable section
 

diff --git a/LeanCamCombi/Mathlib/Logic/Function/Defs.lean b/LeanCamCombi/Mathlib/Logic/Function/Defs.lean
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85",
+   "rev": "27c99fb6e7a1088b1746fe5a63ef1be077b9dd0b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "662f986ad3c5ad6ab1a1726b3c04f5ec425aa9f7",
+   "rev": "a895713f7701e295a015b1087f3113fd3d615272",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -61,11 +61,11 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/siddhartha-gadgil/LeanSearchClient.git",
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "c260ed920e2ebd23ef9fc8ca3fd24115e04c18b1",
+   "scope": "leanprover-community",
+   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "1ea941a98905b2166146b60739226f3953fd5290",
+   "rev": "28af5205699f7d1945d148ebb846cd60a08e74a6",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,