Need feedback on code (metric spaces)

Stream: new members

[Carlos Silva]

Hello. I’ve been working to prove that for metric spaces, being separable is equivalent to being second countable. I am about halfway to proving that and would like feedback on my work so far. I created a lean project, so I believe you can download it by typing
leanproject get carlosa95silva/project
or using the link
https://github.com/carlosa95silva/project .
General structure: I defined a function that outputs a set of balls of the form ball x 1/(n+1) for all x in a given input set. This is a variant of a common construction for metric spaces, but I don’t think it has been given a name and worked with except for theorem  metric.nhds_basis_ball_inv_nat_succ. I go on to prove that if you apply this construction on a dense set, you get a basis.

Here are my questions.

1) I don’t feel like I am making good use of implicit variables in my definitions. I find a lot of theorems won't work unless I use the @ command to spell out the inputs. Does this need fixing?

2) The first two lemmas on lines 15 and 27 expresses trivial facts that I only wrote so I could refer to them in one line later. Was there an easier way?

3) Are there certain code techniques that I am not taking advantage of? I had trouble using simp so I mostly avoided it. Would my code be much better with it?

Thank you for your help.

[Yury G. Kudryashov]

What is your goal? Practice in Lean or formalize something that is not in mathlib yet?

[Yury G. Kudryashov]

We already have docs#emetric.second_countable_of_separable (with most of the work done in docs#uniform_space.second_countable_of_separable).

[Carlos Silva]

@Yury G. Kudryashov My goal was to do both, but I have not looked through the topology folder thoroughly enough to know everything it contains. Thus I might not have written anything useful.

But still for the purpose of practice, I have encountered problems 1,2,3 while writing my code and I don't think I am dealing with those properly. Those I still need advice on.

[Yury G. Kudryashov]

metric.nonempty_ball is supposed to be used as

  have h : (ball x r).nonempty := metric.nonempty_ball.mpr hr_pos,

or

  have h : (ball x r).nonempty, by rwa metric.nonempty_ball,

or

  rw ← metric.nonempty_ball at hr_pos,

[Yury G. Kudryashov]

So, here is one of your proofs as a one-liner without @...s:

open metric

lemma dense_set_int_balls [M : pseudo_metric_space X] (D : set X) (hD : dense D) (x:X) (r:ℝ) ( hr_pos : r>0): set.nonempty ((ball x r) ∩ D) :=
hD.inter_open_nonempty (metric.ball x r) is_open_ball (nonempty_ball.mpr hr_pos)

[Yury G. Kudryashov]

Another technique:

  have h : (ball x r).nonempty, by simpa,

[Yury G. Kudryashov]

Similarly, the first few lines of the next proof can be replaced with

  rw metric.is_open_iff at hU,
  rcases hU x hx with ⟨δ, δ_pos, hball⟩,

or even

  rcases metric.is_open_iff.mp hU x hx with ⟨δ, δ_pos, hball⟩,