Theorem: Tutorial.ContinuousProductTopIff (GlimpseOfLean/Exercises/Topics/GaloisAdjunctions.lean)

State before:
ι : Type
X : ι → Type
T : Π (i : ι), Topology (X i)
Z : Type
TZ : Topology Z
f : Z → Π (i : ι), X i
⊢ Continuous TZ (ProductTopology T) f ↔ ∀ (i : ι), Continuous TZ (T i) fun z => f z i
Tactic:
sorry
State after:
no goals