Continuity points of an upper-semicontinuous compact-valued map are residual

Proved

BCWCentralizer.usc_continuity_points_residual

by Lucas · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

baire-categorydynamical-systemsgeneral-topology

Let $B$ be a Baire space, let $X$ be a compact metric space, and let $\mathcal K(X)$ be the space of non-empty compact subsets of $X$ with the Hausdorff distance $d_H$ . Let $h:B\to\mathcal K(X)$ be upper-semicontinuous: for every $b\in B$ and every open $U\supseteq h(b)$ we have $h(b')\subseteq U$ for all $b'$ in a neighbourhood of $b$ . Then

\{b\in B:\ h \text{ is continuous at } b \text{ for } d_H\}

is a residual subset of $B$ .

This classical fact is the engine of the passage from "dense" to "residual" in Proposition 2.5, applied to $f\mapsto Z^{\mathrm{Lip}}(f)\cap\mathrm{Lip}_K(M)$ .

Formalization Note The paper phrases upper-semicontinuity with sequences ( $b_n\to b\Rightarrow\limsup h(b_n)\subseteq h(b)$ ); the neighbourhood formulation used here is the standard one for compact-valued maps and implies the sequential one.

Preamble

import Mathlib

open scoped Topology

Formal statement

namespace BCWCentralizer
theorem usc_continuity_points_residual {B X : Type*} [TopologicalSpace B] [BaireSpace B]
    [MetricSpace X] [CompactSpace X] (h : B → TopologicalSpace.NonemptyCompacts X)
    (husc : ∀ b : B, ∀ U : Set X, IsOpen U → (h b : Set X) ⊆ U →
      ∀ᶠ b' in 𝓝 b, (h b' : Set X) ⊆ U) :
    {b : B | ContinuousAt h b} ∈ residual B := by sorry
end BCWCentralizer

Source

Bonatti, Crovisier, Wilkinson, *The C^1 generic diffeomorphism has trivial centralizer*, arXiv:0804.1416v1 (2008), https://arxiv.org/abs/0804.1416, p. 16, the classical Proposition quoted in the proof of Proposition 2.5

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent that drafted the Lean statements, with full knowledge of the source paper and of the intended meaning. It is not a blind audit by an independent auditor, and no reviewer should treat it as independent evidence of faithfulness. Please compare it with the Lean code and the source yourself.

Let $B$ be any topological space that is a Baire space, and let $X$ be a metric space that is compact. Let $h$ be any function from $B$ to the set of non-empty compact subsets of $X$ , where this set carries Mathlib's Hausdorff (extended) metric and its topology. Assume: for every $b\in B$ and every open set $U\subseteq X$ with $h(b)\subseteq U$ , the set of $b'\in B$ with $h(b')\subseteq U$ is a neighbourhood of $b$ . Then the set of points $b\in B$ at which $h$ is continuous (for the Hausdorff-metric topology on the target) belongs to the residual filter of $B$ , i.e. it contains a countable intersection of dense open subsets of $B$ . No other hypotheses are made; $B$ may be empty.

Human review

Endorsed by Shuze Chen · Sep 30, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph