mathlib3
feat(analysis/locally_convex/barrel): barreled spaces
#16681
Open
Overview
Commits
349
Changes
View On GitHub

feat(analysis/locally_convex/barrel): barreled spaces #16681

ADedecker wants to merge 349 commits into master from AD_barrels
ADedecker
mcdoll moved file
7ff1ae10
ADedecker ++
1ee006f6
ADedecker Merge remote-tracking branch 'origin/master' into AD_uniform_converge…
a7b63d47
ADedecker Merge remote-tracking branch 'origin/master' into AD_uniform_converge…
b89ec73f
ADedecker ++
78e93a4e
ADedecker `restrict_scalars` for seminorms
cb05339f
ADedecker Continuity criterion for seminorms
8e698289
ADedecker Protect
16eaeb17
ADedecker Unused arguments
255d927d
ADedecker Begin
e4902991
ADedecker Merge remote-tracking branch 'origin/master' into AD_seminorm_continuous
e813095f
ADedecker Begin
acbebc67
ADedecker Closed set characterization of semicontinuous maps to a linear order
6ad87dc7
ADedecker Merge branch 'AD_semicontinuous_closed' into AD_barrels
bc5f09be
ADedecker Progress
c62075ba
ADedecker Closed balls
a300ad54
ADedecker Merge branch 'AD_seminorm_continuous' into AD_barrels
59069292
ADedecker ++
39ef3543
ADedecker Criterions
445b3c23
ADedecker Merge branch 'AD_uniform_convergence_bases' into AD_equicontinuous
adf7fc86
ADedecker Bump, bases
d26dcb40
ADedecker Test
f9fe1039
ADedecker Go back
e3b5bb92
ADedecker Go back again
ca094a23
ADedecker Let's do that later
16829165
ADedecker Progress
20d354e1
ADedecker Closure, finish fixing everything
085ebe3a
ADedecker Uniform equicontinuity on compact spaces
001cb51f
ADedecker Merge remote-tracking branch 'origin/master' into AD_equicontinuous
fba0c8d2
ADedecker Merge remote-tracking branch 'origin/master' into AD_equicontinuous
a4e661bd
ADedecker Docs
86f89e85
YaelDillies backport map_nonneg
0514687e
YaelDillies Merge remote-tracking branch 'origin/master' into kill_normed_group_core
b74d862a
YaelDillies bump
d1f7098e
ADedecker ++
ca1ec0ad
ADedecker Done
f80d9197
ADedecker Merge branch 'AD_uniform_convergence_group' into AD_group_equicontinuity
c8857efb
ADedecker Begin
49263b4e
YaelDillies whooops #lint
0080f108
ADedecker ofSupInf
75b09303
ADedecker Fix
17ee5051
ADedecker Merge remote-tracking branch 'origin/master' into AD_equicontinuous
9d80d077
ADedecker ++
08bc0980
ADedecker Remove exit
8ee0e6bd
ADedecker ++
ab3a65ac
ADedecker Docs
0ca2fd01
ADedecker Merge branch 'AD_seminorm_Sup' into AD_seminorm_equicontinuity
977a776d
ADedecker Faster
db9b3911
ADedecker Merge remote-tracking branch 'origin/master' into AD_seminorm_equicon…
5ccc5ddc
ADedecker Merge branch 'AD_seminorm_Sup' into AD_seminorm_equicontinuity
da5ab0ff
ADedecker Fixes
aa9dc367
ADedecker ++
63f9d5ea
ADedecker Continuity modulus at a point
797c7ad0
ADedecker Merge branch 'AD_equicontinuous' into AD_seminorm_equicontinuity
b3610a75
YaelDillies Merge remote-tracking branch 'origin/master' into kill_normed_group_core
74521c0d
ADedecker Need Yael's code
ae1c772a
ADedecker Merge remote-tracking branch 'origin/kill_normed_group_core' into AD_…
77c2535e
YaelDillies fix analysis.complex.basic
0a298526
ADedecker ++
af9eed59
ADedecker Done
495d347c
ADedecker Merge remote-tracking branch 'origin/kill_normed_group_core' into AD_…
1bf96099
ADedecker Content
8c8d2253
ADedecker Merge branch 'AD_with_seminorms_iff_infi_norms' into AD_seminorm_equi…
e20a6f44
ADedecker Merge remote-tracking branch 'origin/master' into AD_barrels
8a4bd7db
ADedecker Begin
9d76d6c6
ADedecker Clean and simplify
2a2d85da
ADedecker Merge branch 'AD_seminorm_closed_ball' into AD_barrels
f5188e10
ADedecker Clean, part1
3eaba58a
ADedecker ADedecker added WIP
ADedecker Remove unused
937019da
mathlib-dependent-issues-bot mathlib-dependent-issues-bot added blocked-by-other-PR
ADedecker Merge remote-tracking branch 'origin/AD_seminorm_Sup' into AD_barrels
620babdb
ADedecker Progress
b8b18752
ADedecker ++
25ccf42e
ADedecker Begin
edfc11c0
ADedecker Content
b984ce9a
mcdoll Merge branch 'master' into mcdoll/disks
fb9a1874
ADedecker Merge remote-tracking branch 'origin/master' into AD_equicontinuous
5a11ff1f
mcdoll Update src/analysis/locally_convex/basic.lean
72f1a217
ADedecker Iff
becafe80
ADedecker Merge remote-tracking branch 'origin/AD_split_continuous_from_bounded…
b3539ffd
ADedecker ++
c159e066
ADedecker Merge branch 'mcdoll/disks' into AD_hahn_banach
d39f7b4f
ADedecker Oops
3b2719aa
ADedecker Merge remote-tracking branch 'origin/mcdoll/disks' into AD_hahn_banach
fef92630
ADedecker Fix
c782ca6b
ADedecker First step
780c5b6c
ADedecker Finished
b23f32ca
ADedecker Generalize `disjoint.exists_open_convexes` to locally convex spaces
968f45f1
ADedecker Long linea
a959981b
ADedecker Fix
bb804f6a
ADedecker Merge branch 'AD_exists_disjoint_open_convexes' into AD_hahn_banach
7b1d5b51
ADedecker Merge remote-tracking branch 'origin/master' into AD_hahn_banach
c152ed5b
ADedecker Merge remote-tracking branch 'origin/master' into AD_barrels
2d0c6085
ADedecker All LCTVS!
94dd537d
ADedecker Need cache
00232a77
ADedecker Progress
c8de0da5
ADedecker Done
ec63fcc5
ADedecker Need cache again
3a482beb
ADedecker No import
92f273c1
ADedecker Docs
05812ca8
ADedecker Oops
945ce411
ADedecker Merge branch 'AD_closed_or_dense_hyperplane' into AD_hahn_banach
0ab9621c
ADedecker Missing import
ce9861fd
ADedecker Merge branch 'AD_closed_or_dense_hyperplane' into AD_hahn_banach
9fc85607
ADedecker `add_comm_group`
90e1da40
ADedecker Merge branch 'AD_closed_or_dense_hyperplane' into AD_hahn_banach
4f3ff463
ADedecker Done!
cdb1c490
ADedecker Useless import
90dd58c3
ADedecker Generamize Krein-Milman
23d05e9e
ADedecker Merge remote-tracking branch 'origin/AD_hahn_banach' into AD_barrels
245e813c
ADedecker ++
40730f6b
mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed blocked-by-other-PR
mathlib-dependent-issues-bot
ADedecker Merge remote-tracking branch 'origin/master' into AD_barrels
ae7e82a2
ADedecker Fix
e2360c31
ADedecker Merge remote-tracking branch 'origin/master' into AD_equicontinuous
e6e2187d
ADedecker Merge remote-tracking branch 'origin/master' into AD_barrels
58421781
ADedecker Fix
00e50131
ADedecker More progress
97568f98
ADedecker Merge remote-tracking branch 'origin/master' into AD_seminorm_equicon…
a41f5a62
ADedecker Merge remote-tracking branch 'origin/master' into AD_group_equicontin…
296e8d5c
ADedecker Small fixes
0bb30103
ADedecker Fix
c15b879b
ADedecker Fix'
ef9257ba
ADedecker Progress
9c5fa2e2
ADedecker Cleaner
b792fda3
ADedecker Merge branch 'AD_equicontinuous' into AD_seminorm_equicontinuity
46622578
ADedecker Merge remote-tracking branch 'origin/master' into AD_barrels
219b351e
ADedecker ++
fb8010bc
ADedecker Semicontinuity in conditionally complete lattices
ed427a34
ADedecker Merge branch 'AD_upper_semicontinuous_bdd' into AD_barrels
b9d6ebf9
ADedecker ++
ac121fde
ADedecker Progress
e8a70b38
ADedecker Closed-ball characterization of continuity of a seminorm
36e9d8f5
ADedecker Merge branch 'AD_seminorm_continuous_closed_ball' into AD_seminorm_eq…
074f1ac0
ADedecker Step 1 done
343e1d8b
ADedecker 3-week-ago self was dumb
81e8979e
ADedecker Only hard part remaining
d53e327e
ADedecker Going to split
799b983c
ADedecker Fix stupid assumptions
3a27ee6c
ADedecker More related fixes
a6045f9a
ADedecker Initial commt
2b13f669
ADedecker Progress
22404975
ADedecker Switch to "one seminorm first" approach
57750f9b
ADedecker Done!
b36a4bb3
ADedecker Begin semilinearizing `comp`
79001fee
ADedecker Semilinearize `seminorm.comp`
58889133
ADedecker Merge branch 'AD_semilinearize_seminorm_comp' into AD_refactor_shell_…
a06746b3
ADedecker Docs
a3d41a23
ADedecker Closure of `{0}` in a seminormed group
0b39e399
ADedecker Merge branch 'AD_closure_one' into AD_refactor_shell_seminorms
222aab07
ADedecker Docstrings
7409f227
ADedecker ++
06988108
ADedecker Add mem lemma
d1a4b194
ADedecker Merge branch 'AD_closure_one' into AD_refactor_shell_seminorms
0b8967bc
ADedecker Progress
1465689d
ADedecker Swa)
7d57ec3d
ADedecker Merge branch 'AD_closure_one' into AD_refactor_shell_seminorms
63713e0c
ADedecker Fixes
046b0de0
ADedecker Merge branch 'AD_refactor_shell_seminorms' into AD_seminorm_equiconti…
9a07b887
ADedecker Suggestions from review
e2cc5b73
ADedecker Merge remote-tracking branch 'origin/master' into AD_seminorm_continu…
bf299e24
ADedecker Merge remote-tracking branch 'origin/master' into AD_refactor_shell_s…
20ef121b
ADedecker Merge branch 'AD_seminorm_continuous_closed_ball' into AD_refactor_sh…
b9c59be4
ADedecker Merge remote-tracking branch 'origin/master' into AD_equicontinuous
93b1ace7
ADedecker Fix
6b5bf4f3
ADedecker Merge remote-tracking branch 'origin/master' into AD_barrels
2cd9ba9a
ADedecker Fix
fa492907
ADedecker Fixes again
78b49c50
ADedecker Move to new file (I'll write the docstring later)
cbc13830
ADedecker Eventually
f06e8227
ADedecker Add docstringd
8aa578a6
ADedecker Merge branch 'AD_equicontinuous' into AD_group_equicontinuity
3f605b19
ADedecker Merge branch 'AD_refactor_shell_seminorms' into AD_seminorm_equiconti…
bb6b4147
ADedecker Add missing import
81c15ebb
ADedecker Remove now-useless import
78c19f78
ADedecker Proper module docstring
48f151b2
ADedecker Add comment about relative versions
7b7e9633
ADedecker Merge branch 'AD_equicontinuous' into AD_group_equicontinuity
0cf9c5d0
ADedecker Merge branch 'AD_group_equicontinuity' into AD_seminorm_equicontinuity
b28d0d91
ADedecker to_additive
b6b4b642
ADedecker Merge branch 'AD_group_equicontinuity' into AD_seminorm_equicontinuity
b44bdc41
ADedecker Make linter happy
0bef1ecd
ADedecker Start
b20c412a
ADedecker Full test, part 1
cb9a9395
ADedecker ++
f89ac58f
ADedecker Update docstrings for first half of file
34b7305a
ADedecker Update dosctrings in second half of file
7b257abe
ADedecker Remove commented code
5b18a4f1
ADedecker Update module docstring
eb686f03
ADedecker Update docstrings in `topology/algebra/uniform_convergence`
c29b3a73
ADedecker Update `topology/algebra/module/strong_topology`
4d32b0ee
ADedecker Add TODO
c8a2db40
ADedecker Merge branch 'AD_uniform_continuous_type_alias' into AD_equicontinuous
550844c5
ADedecker Merge branch 'AD_equicontinuous' into AD_group_equicontinuity
4793c504
ADedecker Merge branch 'AD_group_equicontinuity' into AD_seminorm_equicontinuity
4fcf0db0
ADedecker Fixes, part1
2a1a84d6
ADedecker All fixed?
d4e15837
ADedecker Merge remote-tracking branch 'origin/AD_equicontinuous' into AD_group…
3584afbb
ADedecker Merge branch 'AD_equicontinuous' into AD_seminorm_equicontinuity
eb4b1e8c
ADedecker Last fixes
457acd16
ADedecker Merge remote-tracking branch 'origin/AD_equicontinuous' into AD_group…
a893d47f
ADedecker Merge branch 'AD_group_equicontinuity' into AD_seminorm_equicontinuity
6e4259af
ADedecker Fixes
05ea2ce8
ADedecker Merge branch 'AD_group_equicontinuity' into AD_seminorm_equicontinuity
790854a4
ADedecker Fix again
0a41de15
ADedecker Merge remote-tracking branch 'origin/master' into AD_seminorm_continu…
0ed68d92
ADedecker Merge remote-tracking branch 'origin/master' into AD_refactor_shell_s…
76dbdb53
ADedecker Fix
a419cb93
ADedecker Merge branch 'AD_seminorm_continuous_closed_ball' into AD_refactor_sh…
6b29a278
ADedecker Fix
688a8c67
ADedecker More norm breakage
fa4565a7
ADedecker Merge branch 'AD_refactor_shell_seminorms' into AD_seminorm_equiconti…
a4eb4f8e
ADedecker Fix Ascoli
81426cce
ADedecker Merge branch 'AD_equicontinuous' into AD_seminorm_equicontinuity
f60f857a
ADedecker Merge branch 'AD_seminorm_equicontinuity' into AD_barrels
99463e68
ADedecker First fixes
ad0725f1
ADedecker Fix, comment dead code
d2c959d9
ADedecker Merge branch 'AD_seminorm_equicontinuity' into AD_barrels
ff11525a
ADedecker Clean
95aefdb2
ADedecker Generalize radius
41ff1bee
ADedecker Eric's suggestions
3a87b89b
ADedecker Floris's sugestions
8dbbcc27
ADedecker Useless ()
53309d8d
ADedecker More variations for closure
7befa296
ADedecker Add a few more lemmas
001e3d4c
ADedecker Merge branch 'AD_equicontinuous' into AD_group_equicontinuity
973de836
ADedecker Merge branch 'AD_group_equicontinuity' into AD_seminorm_equicontinuity
29cb7dda
ADedecker Merge branch 'AD_seminorm_equicontinuity' into AD_barrels
0b0d343c
ADedecker Fix again
a0621a70
ADedecker Merge branch 'AD_equicontinuous' into AD_group_equicontinuity
828c64fa
ADedecker Merge branch 'AD_group_equicontinuity' into AD_seminorm_equicontinuity
7104ea56
ADedecker Merge branch 'AD_seminorm_equicontinuity' into AD_barrels
be124f0e
ADedecker Merge remote-tracking branch 'origin/master' into AD_barrels
54ab7f6f
ADedecker Merge remote-tracking branch 'origin/master' into AD_refactor_shell_s…
a058e58e
ADedecker Merge branch 'AD_seminorm_continuous_closed_ball' into AD_refactor_sh…
a62881a1
ADedecker Merge remote-tracking branch 'origin/master' into AD_refactor_shell_s…
f36fbba4
ADedecker Merge remote-tracking branch 'origin/master' into AD_refactor_shell_s…
75f95122
ADedecker Fix1
3f54becb
ADedecker ++
1ae42b61
ADedecker More fixes
1ac6cf57
ADedecker Merge branch 'AD_refactor_shell_seminorms' into AD_seminorm_equiconti…
24ec27d1
ADedecker Merge remote-tracking branch 'origin/master' into AD_refactor_shell_s…
9a679c38
ADedecker Move things around
e9c4fade
ADedecker Add a todo
d1d57fd7
ADedecker Merge branch 'AD_refactor_shell_seminorms' into AD_seminorm_equiconti…
9743dab7
ADedecker Long line
68219f97
ADedecker Merge remote-tracking branch 'origin/master' into AD_refactor_shell_s…
a71ea2d7
ADedecker Merge remote-tracking branch 'origin/master' into AD_refactor_shell_s…
362dc7b7
ADedecker Update src/analysis/locally_convex/with_seminorms.lean
5da63a98
ADedecker Fix comment
37837dc8
ADedecker Merge branch 'AD_refactor_shell_seminorms' into AD_seminorm_equiconti…
dbde88c8
ADedecker Merge branch 'AD_seminorm_equicontinuity' into AD_barrels
e90f806e
github-actions github-actions added modifies-synchronized-file
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
WIP modifies-synchronized-file too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum