rw [lowerBounds_range]
ι : Type
X : ι → Type
T : Π (i : ι), Topology (X i)
Z : Type
TZ : Topology Z
f : Z → Π (i : ι), X i
⊢ f⁎ TZ ∈ lowerBounds (Set.range fun i => (fun x => x i)^* (T i)) ↔ ∀ (i : ι), f⁎ TZ ≤ (fun x => x i)^* (T i)
no goals