α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type ?u.49234
ζ : Type ?u.49237
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
⊢ induced Prod.fst (induced f inst✝⁴) ⊓ induced Prod.snd (induced g inst✝²) =
    induced (fun p => (f p.fst, g p.snd)) (induced Prod.fst inst✝⁴ ⊓ induced Prod.snd inst✝²)
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type ?u.49234
ζ : Type ?u.49237
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
⊢ instTopologicalSpaceProd = induced (fun p => (f p.fst, g p.snd)) instTopologicalSpaceProd
delta instTopologicalSpaceProd
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type ?u.49234
ζ : Type ?u.49237
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
⊢ induced (f ∘ Prod.fst) inst✝⁴ ⊓ induced (g ∘ Prod.snd) inst✝² =
    induced (Prod.fst ∘ fun p => (f p.fst, g p.snd)) inst✝⁴ ⊓ induced (Prod.snd ∘ fun p => (f p.fst, g p.snd)) inst✝²
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type ?u.49234
ζ : Type ?u.49237
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
⊢ induced Prod.fst (induced f inst✝⁴) ⊓ induced Prod.snd (induced g inst✝²) =
    induced (fun p => (f p.fst, g p.snd)) (induced Prod.fst inst✝⁴ ⊓ induced Prod.snd inst✝²)
simp_rw [induced_inf, induced_compose]
no goals
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type ?u.49234
ζ : Type ?u.49237
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
⊢ induced (f ∘ Prod.fst) inst✝⁴ ⊓ induced (g ∘ Prod.snd) inst✝² =
    induced (Prod.fst ∘ fun p => (f p.fst, g p.snd)) inst✝⁴ ⊓ induced (Prod.snd ∘ fun p => (f p.fst, g p.snd)) inst✝²
rfl