x y : SimplexCategory
f : x ⟶ y
i : (CategoryTheory.forget SimplexCategory).obj y
⊢ Continuous fun a =>
    ∑ j in Finset.filter (fun k => (CategoryTheory.forget SimplexCategory).map f k = i) Finset.univ, ↑a j
x y : SimplexCategory
f : x ⟶ y
⊢ Continuous (toTopMap f)
refine' Continuous.subtype_mk (continuous_pi fun i => _) _
x y : SimplexCategory
f : x ⟶ y
i : (CategoryTheory.forget SimplexCategory).obj y
⊢ Continuous fun a =>
    ∑ j in Finset.filter (fun k => (CategoryTheory.forget SimplexCategory).map f k = i) Finset.univ, ↑a j
x y : SimplexCategory
f : x ⟶ y
i : (CategoryTheory.forget SimplexCategory).obj y
⊢ Continuous fun a =>
    ∑ j in Finset.filter (fun k => (CategoryTheory.forget SimplexCategory).map f k = i) Finset.univ, ↑a j
dsimp only [coe_toTopMap]
no goals
x y : SimplexCategory
f : x ⟶ y
i : (CategoryTheory.forget SimplexCategory).obj y
⊢ Continuous fun a =>
    ∑ j in Finset.filter (fun k => (CategoryTheory.forget SimplexCategory).map f k = i) Finset.univ, ↑a j
exact continuous_finset_sum _ (fun j _ => (continuous_apply _).comp continuous_subtype_val)