uniform_convergence_topology): `𝔖`-convergence depends only on the bornology generated by `𝔖`
#18009

Open

feat(topology/uniform_space/uniform_convergence_topology): `𝔖`-convergence depends only on the bornology generated by `𝔖` #18009

ADedecker wants to merge 9 commits into master from AD_uniform_convergence_generated_bornology

Initial commit

4cdb798b

First part done

ff0d0dd2

Initial commit

1fce757a

More progress

0c945817

Done?

e791b928

Done?

ad6bbd2f

ADedecker added WIP

ADedecker added t-topology

Fix

e80bbbe4

ADedecker marked this pull request as ready for review 3 years ago

ADedecker removed WIP

ADedecker added awaiting-review

PatrickMassot commented on 2023-01-17

leanprover-community-bot-assistant added delegated

leanprover-community-bot-assistant removed awaiting-review

Merge remote-tracking branch 'origin/master' into AD_uniform_converge…

8fd8f445

Merge remote-tracking branch 'origin/master' into AD_uniform_converge…

76f15230

github-actions added modifies-synchronized-file

kim-em added too-late

Reviewers

PatrickMassot

Assignees

No one assigned

Labels

delegated t-topology modifies-synchronized-file too-late

Milestone

No milestone