feat(category_theory/limits): is_iso_π_of_is_initial (#6908)
feat(category_theory/limits): is_iso_π_of_is_initial (#6908)

From [zulip](https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/Simplicial.20stuff/near/231346653)



Co-authored-by: Scott Morrison <63f04b4d96235eb042cc46d94f14d241d2a26722@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib