Theorems · Theorem · general topology

ContinuousMap.exists_finite_sum_const_mulIndicator_approximation_of_mem_nhds_diagonal

∀ {X : Type u_1} {V : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace V] [TotallyDisconnectedSpace X]
  [T2Space X] [CompactSpace X] {S : Set (V × V)} (f : C(X, V)) [inst_5 : CommMonoid V],
  S ∈ nhdsSet (Set.diagonal V) → ∃ n U v, ∀ (x : X), (f x, ∏ n, (↑(U n)).mulIndicator (fun x => v n) x) ∈ S

If f is a continuous map from a profinite space to a topological space with a commutative monoid structure, then we can approximate f by finite products of indicator functions of clopen sets. (Note no compatibility is assumed between the monoid structure on V and the topology.)

Defined in

Mathlib.Topology.Separation.DisjointCover

Cited by

0 results in Mathlib

Foundations

Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceTotallyDisconnectedSpaceT2SpaceCompactSpaceCommMonoid