Anatole Dedecker comments

Results 25 comments of


                                            Anatole Dedecker

trafficstars

feat(topology/uniform_space/uniform_convergence_topology): continuity of [pre,post]composition, and other topological properties

bors r+

feat(topology/uniform_space/uniform_convergence_topology): continuity of [pre,post]composition, and other topological properties

bors cancel

feat(topology/uniform_space/uniform_convergence_topology): continuity of [pre,post]composition, and other topological properties

bors r+

refactor(analysis/normed/group/basic): generalize `(semi)normed_add_comm_group.induced` to `add_monoid_hom_class` and add more tools to pull back norm structures

Could you fix the conflicts?

refactor(analysis/normed/group/basic): generalize `(semi)normed_add_comm_group.induced` to `add_monoid_hom_class` and add more tools to pull back norm structures

> I have also added the `norm_one_class` and `normed_algebra` results. Sorry, I don't see them :sweat_smile: Git mistake maybe?

refactor(analysis/normed/group/basic): generalize `(semi)normed_add_comm_group.induced` to `add_monoid_hom_class` and add more tools to pull back norm structures

Thanks! maintainer merge

feat(analysis/normed_space/hahn_banach/separation): generalize to (locally convex) topological vector spaces

About moving files: everything in `hahn_banach/separation` now works in any locally convex space, so we just have to discuss moving the full file. I'd argue that we definitely want to...

feat(analysis/normed_space/hahn_banach/separation): generalize to (locally convex) topological vector spaces

Let's leave it there for now then.

feat(topology/algebra/module/basic): a hyperplane is either closed or dense

bors r+

feat(topology/algebra/module/strong_operator, analysis/normed_space/operator_norm): strong operator topology

> I guess it would be nice to see the topology in action Is there anything in particular you'd like to have? I must say this has been waiting for...