Theorems · Theorem · general topology

ContinuousMap.exists_disjoint_nonempty_clopen_cover_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 D,
      (∀ (i : Fin n), D i ≠ ⊥) ∧
        (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (f y, f z) ∈ S) ∧
          Set.univ ⊆ ⋃ i, ↑(D i) ∧ Pairwise (Function.onFun Disjoint D)

For any continuous function f : X → V, with X profinite, and S a neighbourhood of the diagonal in V × V, there exists a finite cover of X by pairwise-disjoint nonempty clopens, on each of which f varies within S.

Defined in

Mathlib.Topology.Separation.DisjointCover

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTotallyDisconnectedSpaceT2SpaceCompactSpace