Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
77 commits
Select commit Hold shift + click to select a range
b2938f4
copy paste
DavidLedvinka Jun 21, 2025
787c11d
remove check
DavidLedvinka Jun 21, 2025
91b194b
changed file name
DavidLedvinka Jun 21, 2025
eb5e2e7
finished documentation
DavidLedvinka Jun 21, 2025
3e003db
add definition docs
DavidLedvinka Jun 21, 2025
405769f
fix doc
DavidLedvinka Jun 21, 2025
8f1391a
more doc
DavidLedvinka Jun 21, 2025
fd2c7a1
fix typo
DavidLedvinka Jun 21, 2025
7289624
another doc fix
DavidLedvinka Jun 21, 2025
a7abfeb
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
b73da8c
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
e411d6c
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
b0f9963
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
3c8b357
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
1e52ab9
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
06400ce
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
a3e56e0
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
d077d98
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
5c8e624
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
e9fd582
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
bbb0b35
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
30dbe1a
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
b67b372
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
85e08bf
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
a246002
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
27b00e0
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
3625242
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
f22fac5
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
0f7cde5
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
0cb248d
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
874ba3c
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
e68ccf2
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 17, 2025
877cf75
review edits
DavidLedvinka Jul 18, 2025
c314a58
delete accidentally added file
DavidLedvinka Jul 18, 2025
fc28056
grw refactor
DavidLedvinka Jul 18, 2025
0c3b068
slight golfs
DavidLedvinka Jul 18, 2025
37456f8
add backticks for math
DavidLedvinka Jul 18, 2025
ccab12a
more fixes
DavidLedvinka Jul 18, 2025
27c7fff
Merge branch 'master' of https://github.com/leanprover-community/math…
DavidLedvinka Jul 18, 2025
2c9a62e
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 18, 2025
c3cf121
integrate Etienne's proof
DavidLedvinka Jul 18, 2025
5f6aa38
Update lake-manifest.json
DavidLedvinka Jul 18, 2025
87ebf37
remove unused argument
DavidLedvinka Jul 18, 2025
b2f1ab7
fix imports
DavidLedvinka Jul 18, 2025
2ed0757
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Jul 26, 2025
a883cab
namespace
DavidLedvinka Jul 26, 2025
f9a56ba
Merge branch 'master' into logSizeBallSequence
RemyDegenne Aug 10, 2025
b9bc3b4
add docstring
RemyDegenne Aug 10, 2025
9bab265
remove 1 < a hypothesis
RemyDegenne Aug 10, 2025
516e558
explicit arg
RemyDegenne Aug 10, 2025
7f24cd5
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Aug 14, 2025
49c2147
Merge branch 'leanprover-community:master' into logSizeBallSequence
DavidLedvinka Aug 14, 2025
3acf6d0
apply fixes
DavidLedvinka Aug 14, 2025
e8420de
apply fixes
DavidLedvinka Aug 14, 2025
bee89b2
simp proof more
DavidLedvinka Aug 14, 2025
cf12f99
Merge branch 'leanprover-community:master' into logSizeBallSequence
DavidLedvinka Aug 20, 2025
dba50f7
test
DavidLedvinka Oct 9, 2025
536d4cc
Merge branch 'master' into pdf_mul
DavidLedvinka Oct 9, 2025
56b8667
test
DavidLedvinka Oct 9, 2025
18ebef6
Update lake-manifest.json
DavidLedvinka Oct 10, 2025
3c138ef
improve doc WIP
DavidLedvinka Oct 15, 2025
6633b19
complete doc
DavidLedvinka Oct 15, 2025
a0048d1
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Oct 15, 2025
47d6497
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Oct 15, 2025
b292eaf
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Oct 15, 2025
d838b9e
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Oct 15, 2025
1fac378
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Oct 15, 2025
5f02ad2
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Oct 15, 2025
9b82dc4
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Oct 15, 2025
48f77f9
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Oct 15, 2025
2e32a43
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Oct 15, 2025
caa472f
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Oct 15, 2025
7aba02a
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Oct 15, 2025
5c5a589
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Oct 15, 2025
09487af
Update Mathlib/Topology/EMetricSpace/PairReduction.lean
DavidLedvinka Oct 15, 2025
8b02bc2
update
DavidLedvinka Oct 15, 2025
cd912c3
add EMetric namespace
DavidLedvinka Oct 16, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -6656,6 +6656,7 @@ import Mathlib.Topology.EMetricSpace.BoundedVariation
import Mathlib.Topology.EMetricSpace.Defs
import Mathlib.Topology.EMetricSpace.Diam
import Mathlib.Topology.EMetricSpace.Lipschitz
import Mathlib.Topology.EMetricSpace.PairReduction
import Mathlib.Topology.EMetricSpace.Paracompact
import Mathlib.Topology.EMetricSpace.Pi
import Mathlib.Topology.ExtendFrom
Expand Down
Loading
Loading