Commit 2023-01-26 19:20 467e1558

feat: port Topology.Bornology.Basic (#1822) porting notes:

1. There were two places where Lean couldn't figure out the type class (Bornology) arguments to isBounded_def when used within a rewrite or simp lemma, and I had to provide these explicitly. I have worked around it for now (by supplying those arguments), but Lean 3 did not have this problem and we should investigate the issue.
2. Because Lean 4 does not accept the [] syntax in structure fields to make arguments explicit, it was necessary to rename the structure fields and then provide new Bornology.cobounded and Bornology.le_cofinite declarations with the type argument explicit. See the discussion here: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Topology.2EBornology.2EBasic