exact Iff.rfl
ι : Type
X : ι → Type
T : Π (i : ι), Topology (X i)
Z : Type
TZ : Topology Z
f : Z → Π (i : ι), X i
⊢ Continuous TZ (ProductTopology T) f ↔ f⁎ TZ ≤ Inf (Set.range fun i => (fun x => x i)^* (T i))
no goals