Theorems · Theorem · general topology

ContinuousMap.exists_finite_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)),
  S ∈ nhdsSet (Set.diagonal V) → ∃ n g h, Continuous g ∧ ∀ (x : X), (f x, h (g x)) ∈ S

For any continuous function f : X → V, with X profinite, and S a neighbourhood of the diagonal in V × V, the function f can be S-approximated by a function factoring through Fin n, for some n.

Defined in

Mathlib.Topology.Separation.DisjointCover

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTotallyDisconnectedSpaceT2SpaceCompactSpace