mathlib3 documentation

topology.category.Profinite.cofiltered_limit

Cofiltered limits of profinite sets. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains some theorems about cofiltered limits of profinite sets.

Main Results #

If X is a cofiltered limit of profinite sets, then any clopen subset of X arises from a clopen set in one of the terms in the limit.

Any locally constant function from a cofiltered limit of profinite sets factors through one of the components.