Skip to content

Commit

Permalink
Bump mathlib
Browse files Browse the repository at this point in the history
  • Loading branch information
YaelDillies committed Jun 25, 2024
1 parent 1a30ed2 commit 227ebd6
Show file tree
Hide file tree
Showing 13 changed files with 7 additions and 318 deletions.
5 changes: 0 additions & 5 deletions LeanCamCombi.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@ import LeanCamCombi.BernoulliSeq
import LeanCamCombi.ConvexContinuous
import LeanCamCombi.Corners.CombiDegen
import LeanCamCombi.DiscreteDeriv
import LeanCamCombi.ErdosGinzburgZiv
import LeanCamCombi.ErdosRenyi.Basic
import LeanCamCombi.ErdosRenyi.BollobasContainment
import LeanCamCombi.ErdosRenyi.Connectivity
Expand All @@ -18,7 +17,6 @@ import LeanCamCombi.Kneser.Mathlib
import LeanCamCombi.Kneser.MulStab
import LeanCamCombi.KruskalKatona
import LeanCamCombi.LittlewoodOfford
import LeanCamCombi.Mathlib.Algebra.BigOperators.Ring
import LeanCamCombi.Mathlib.Algebra.Order.BigOperators.LocallyFinite
import LeanCamCombi.Mathlib.Analysis.Convex.Exposed
import LeanCamCombi.Mathlib.Analysis.Convex.Extreme
Expand All @@ -27,7 +25,6 @@ import LeanCamCombi.Mathlib.Analysis.Convex.Independence
import LeanCamCombi.Mathlib.Analysis.Convex.Normed
import LeanCamCombi.Mathlib.Analysis.Convex.Segment
import LeanCamCombi.Mathlib.Analysis.Convex.SimplicialComplex.Basic
import LeanCamCombi.Mathlib.Analysis.Normed.Group.Basic
import LeanCamCombi.Mathlib.Combinatorics.Colex
import LeanCamCombi.Mathlib.Combinatorics.Schnirelmann
import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Shatter
Expand All @@ -41,7 +38,6 @@ import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Multipartite
import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
import LeanCamCombi.Mathlib.Data.Finset.Pointwise
import LeanCamCombi.Mathlib.Data.Finset.PosDiffs
import LeanCamCombi.Mathlib.Data.Int.Defs
import LeanCamCombi.Mathlib.Data.List.Basic
import LeanCamCombi.Mathlib.Data.List.DropRight
import LeanCamCombi.Mathlib.Data.Multiset.Basic
Expand All @@ -56,7 +52,6 @@ import LeanCamCombi.Mathlib.Order.Sublattice
import LeanCamCombi.Mathlib.Probability.Independence.Basic
import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
import LeanCamCombi.Mathlib.RingTheory.Int.Basic
import LeanCamCombi.Mathlib.Topology.Algebra.Group.Basic
import LeanCamCombi.MetricBetween
import LeanCamCombi.MinkowskiCaratheodory
import LeanCamCombi.SimplicialComplex.Basic
Expand Down
4 changes: 2 additions & 2 deletions LeanCamCombi/ConvexContinuous.lean
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,9 @@ Authors: Yaël Dillies
-/
import Mathlib.Analysis.Convex.Intrinsic
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.Normed.Group.Basic
import Mathlib.Topology.Algebra.Group.Basic
import LeanCamCombi.Mathlib.Analysis.Convex.Normed
import LeanCamCombi.Mathlib.Analysis.Normed.Group.Basic
import LeanCamCombi.Mathlib.Topology.Algebra.Group.Basic

/-!
# Convex functions are continuous
Expand Down
186 changes: 0 additions & 186 deletions LeanCamCombi/ErdosGinzburgZiv.lean

This file was deleted.

30 changes: 0 additions & 30 deletions LeanCamCombi/Mathlib/Algebra/BigOperators/Ring.lean

This file was deleted.

2 changes: 1 addition & 1 deletion LeanCamCombi/Mathlib/Analysis/Convex/Segment.lean
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import Mathlib.Analysis.Convex.Segment
import Mathlib.Topology.MetricSpace.PseudoMetric
import Mathlib.Topology.MetricSpace.Pseudo.Defs

namespace Real
variable {ε r : ℝ}
Expand Down
24 changes: 0 additions & 24 deletions LeanCamCombi/Mathlib/Analysis/Normed/Group/Basic.lean

This file was deleted.

6 changes: 0 additions & 6 deletions LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,6 @@ open Set
variable {α β : Type*} {G H : SimpleGraph α} {s : Set (Sym2 α)}

namespace SimpleGraph

@[simp]
lemma deleteEdges_eq_self {s : Set (Sym2 α)} : G.deleteEdges s = G ↔ Disjoint G.edgeSet s := by
rw [deleteEdges, sdiff_eq_left, disjoint_fromEdgeSet]
#align simple_graph.delete_edges_eq SimpleGraph.deleteEdges_eq_self

section Ind
variable {s t : Set α} {a b : α}

Expand Down
40 changes: 0 additions & 40 deletions LeanCamCombi/Mathlib/Data/Int/Defs.lean

This file was deleted.

20 changes: 0 additions & 20 deletions LeanCamCombi/Mathlib/Topology/Algebra/Group/Basic.lean

This file was deleted.

2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,6 @@ The project contains

The following topics are under active development in LeanCamCombi.

* The Erdős-Ginzburg-Ziv theorem
* The Erdős-Rényi model for random graphs, aka binomial random graph
* The Littlewood-Offord problem
* The van den Berg-Kesten-Reimer inequality
Expand Down Expand Up @@ -68,6 +67,7 @@ The following topics have been upstreamed to mathlib and no longer live in LeanC
* The four functions theorem and related discrete correlation inequalities: FKG inequality, Holley inequality, Daykin inequality, Marica-Schönheim inequality
* The Birkhoff representation theorem, non-categorical version
* The Cauchy-Davenport theorem for general groups, and also for linearly ordered cancellative semigroup
* The Erdős-Ginzburg-Ziv theorem
* Shatterings of sets, the Sauer-Shelah lemma and the Vapnik-Chervonenkis dimension
* Sublattices
* Strongly convex functions
Expand Down
Loading

0 comments on commit 227ebd6

Please sign in to comment.