topology rational addition is continuous

Stream: maths

[RustyYato]

I'm trying to prove that addition over the rationals is continuous in both arguments.
But I'm now sure how to proceed. I think there is something I am fundamentally misunderstanding about how the product topology works.

Here's a MWE of what I'm trying to prove. I know that the line this proof went down is hopeless, but I'm not sure what else I can do.
(NOTE: I would like to avoid using rat_add_continuous_lemma, since I'm trying to learn to do this myself).

import Mathlib.Topology.Constructions
import Mathlib.Topology.Instances.Rat

open TopologicalSpace

instance : Continuous (fun x: ℚ × ℚ => x.fst + x.snd) where
  isOpen_preimage := by
    intro S S_open
    apply GenerateOpen.basic
    dsimp
    left
    dsimp
    refine ⟨S, S_open, ?_⟩
    sorry -- what to do now?

[RustyYato]

I was able to prove that it's continuous in each argument separately (i.e. fun x: ℚ => x + a with some fixed a). But not when generalizing to above.

[Jireh Loreaux]

The answer is that there are 15 different ways to prove this result. The key question is: what is the proof on paper that you want to formalize? The answer to that will influence the advice we give.

(e.g., do you want to use a standard ε and δ proof? Is there a reason you chose ℚ specifically, and not ℝ?)

[RustyYato]

Yes, a standard ε-δproof will work. I've chosen ℚ because, in reality, I'm not directly using mathlib. I'm just using it as a reference, and am writing out the proofs myself, sometimes making slightly different decisions from mathlib.

At this point, I don't have ℝ setup enough to be viable, and as part of that I'm building out my theories on ℚ.