Commit 2021-06-22 14:51 7e20058e

View on Github →

feat(topology/Profinite/cofiltered_limit): Locally constant functions from cofiltered limits (#7992) This generalizes one of the main technical theorems from LTE about cofiltered limits of profinite sets. This theorem should be useful for a future proof of Stone duality.

Estimated changes

Modified src/topology/category/Profinite/cofiltered_limit.lean

added theorem Profinite.exists_locally_constant

added theorem Profinite.exists_locally_constant_fin_two

added theorem Profinite.exists_locally_constant_fintype_aux

added theorem Profinite.exists_locally_constant_fintype_nonempty

Modified src/topology/discrete_quotient.lean

added def locally_constant.discrete_quotient

added theorem locally_constant.factors

added def locally_constant.lift

added theorem locally_constant.lift_eq_coe

added theorem locally_constant.lift_is_locally_constant

added def locally_constant.locally_constant_lift

Modified src/topology/locally_constant/basic.lean

added theorem is_locally_constant.is_clopen_fiber

added theorem is_locally_constant.is_closed_fiber