Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: port Topology.Basic #1826

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - feat: port Topology.Basic #1826

Show file tree
Hide file tree
Changes from 9 commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
9d19930
feat: port Topology.Basic
urkud Jan 25, 2023
353f65f
Initial file copy from mathport
urkud Jan 25, 2023
0ba17e4
automated fixes
urkud Jan 25, 2023
5ddc5c4
Drop dependency on `pfun`
urkud Jan 25, 2023
d93dc1c
Fix most of the file
urkud Jan 25, 2023
0cbd7fc
Fix `lim`s
urkud Jan 25, 2023
9722c39
Fix comments (auto+manually)
urkud Jan 25, 2023
ba1dab9
drop a long line
urkud Jan 25, 2023
7f8aebc
Fix linter
urkud Jan 25, 2023
66677e2
Apply suggestions from code review
urkud Jan 25, 2023
c72fea5
limUnder
jcommelin Jan 26, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -824,6 +824,7 @@ import Mathlib.Tactic.Zify.Attr
import Mathlib.Testing.SlimCheck.Gen
import Mathlib.Testing.SlimCheck.Sampleable
import Mathlib.Testing.SlimCheck.Testable
import Mathlib.Topology.Basic
import Mathlib.Util.AtomM
import Mathlib.Util.Export
import Mathlib.Util.IncludeStr
Expand Down