mathlib3
feat(topology/inseparable): Define `specializing` maps between topological spaces
#17113
Open
Open
feat(topology/inseparable): Define `specializing` maps between topological spaces #17113
erdOne
wants to merge
16 commits into
master
from
specialising_map
first commit
411d4f26
address comments
9f25cbee
Update upper_lower.lean
643cc9d8
alreadydone
changed the title
address comments
562c3c95
Merge branch 'specialising_map' of https://github.com/leanprover-comm…
bcd99b5e
Apply suggestions from code review
4ee55898
Update src/topology/inseparable.lean
e85727b4
docstrings, aliases
04ce7564
alreadydone
commented
on 2022-10-26
urkud
commented
on 2022-10-29
Change docstring
59d200ae
address comments
5d79d510
remove `_root_`
f75f3118
remove lemmas
0a8ccd9c
fix and rename
a59c65b5
Update src/order/upper_lower.lean
adb37dc4
YaelDillies
commented
on 2022-11-19
replace lemmas
701b1fc2
Merge branch 'specialising_map' of https://github.com/leanprover-comm…
e9e08fae
YaelDillies
commented
on 2022-11-20
jcommelin
approved these changes
on 2022-12-07
Reviewers
Assignees
No one assigned
Labels
awaiting-author
t-topology
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub