intro i
case h
ι : Type
X : ι → Type
T : Π (i : ι), Topology (X i)
Z : Type
TZ : Topology Z
f : Z → Π (i : ι), X i
⊢ ∀ (a : ι), f⁎ TZ ≤ (fun x => x a)^* (T a) ↔ (fun x => x a)⁎ (f⁎ TZ) ≤ T a
case h
ι : Type
X : ι → Type
T : Π (i : ι), Topology (X i)
Z : Type
TZ : Topology Z
f : Z → Π (i : ι), X i
i : ι
⊢ f⁎ TZ ≤ (fun x => x i)^* (T i) ↔ (fun x => x i)⁎ (f⁎ TZ) ≤ T i