α : Type u
β : Type v
γ : Type ?u.512017
δ : Type ?u.512020
ε : Type ?u.512023
ζ : Type ?u.512026
ι : Type u_2
π : ι → Type u_3
κ : Type ?u.512037
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f✝ : α → (i : ι) → π i
X : Type u_1
f : X → (i : ι) → π i
⊢ (⨅ (i : ι), induced f (induced (fun f => f i) ((fun a => inst✝ a) i))) =
    ⨅ (i : ι), induced (fun x => f x i) inferInstance
α : Type u
β : Type v
γ : Type ?u.512017
δ : Type ?u.512020
ε : Type ?u.512023
ζ : Type ?u.512026
ι : Type u_2
π : ι → Type u_3
κ : Type ?u.512037
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f✝ : α → (i : ι) → π i
X : Type u_1
f : X → (i : ι) → π i
⊢ induced f Pi.topologicalSpace = ⨅ (i : ι), induced (fun x => f x i) inferInstance
erw [induced_iInf]
α : Type u
β : Type v
γ : Type ?u.512017
δ : Type ?u.512020
ε : Type ?u.512023
ζ : Type ?u.512026
ι : Type u_2
π : ι → Type u_3
κ : Type ?u.512037
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f✝ : α → (i : ι) → π i
X : Type u_1
f : X → (i : ι) → π i
⊢ (⨅ (i : ι), induced ((fun f => f i) ∘ f) (inst✝ i)) = ⨅ (i : ι), induced (fun x => f x i) inferInstance
α : Type u
β : Type v
γ : Type ?u.512017
δ : Type ?u.512020
ε : Type ?u.512023
ζ : Type ?u.512026
ι : Type u_2
π : ι → Type u_3
κ : Type ?u.512037
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f✝ : α → (i : ι) → π i
X : Type u_1
f : X → (i : ι) → π i
⊢ (⨅ (i : ι), induced f (induced (fun f => f i) ((fun a => inst✝ a) i))) =
    ⨅ (i : ι), induced (fun x => f x i) inferInstance
simp only [induced_compose]
no goals
α : Type u
β : Type v
γ : Type ?u.512017
δ : Type ?u.512020
ε : Type ?u.512023
ζ : Type ?u.512026
ι : Type u_2
π : ι → Type u_3
κ : Type ?u.512037
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f✝ : α → (i : ι) → π i
X : Type u_1
f : X → (i : ι) → π i
⊢ (⨅ (i : ι), induced ((fun f => f i) ∘ f) (inst✝ i)) = ⨅ (i : ι), induced (fun x => f x i) inferInstance
rfl