mathlib

7e281def - feat(topology/extremally_disconnected): Extremally disconnected topological spaces (#8196)

feat(topology/extremally_disconnected): Extremally disconnected topological spaces (#8196) From LTE Author: Johan Commelin [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/extremally.20disconnected.20sets) Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>