Commit 2025-12-17 18:54 4947a3a5

refactor: generalize semicontinuity (#32521) This PR redefines (although defeq to the original) upper and lower semicontinuity in terms of a new predicate Semicontinuous which takes a relation r : α → β → Prop instead of a function f : α → β. We say that a relation r is semicontinuous at x within s if ∀ y, r x y → ∀ᶠ x' in 𝓝[s], r x' y. In other words, if the relation holds for a pair x : α and y : β, then it also holds for all x' (with the same y) sufficiently near to x within s. To recover lower or upper semicontinuity, the relation chosen is r := (f · > ·) or r := (f · < ·), respectively. Note that semicontinuity of r at x within s is equivalent to ∀ y, (∃ᶠ x' in 𝓝[s] x, ¬ r x' y) → ¬ r x y, so one may freely switch between the eventual or the frequent characterization at the cost of negation of the relation r. The purpose behind this refactor is to allow a common definition not only for lower and upper semicontinuity, but also for lower and upper hemicontinuity (for those unfamiliar, this should be thought of as lower and upper semicontinuity for set-valued functions). This was discussed on Zulip a while ago here: #maths > upper hemicontinuity vs. upper semicontinuity. Although the number of lemmas shared between all versions is not particularly high, it's nice to avoid some boilerplate, and to show that all these concepts can be unified. Given a set-valued function f : α → Set β, lower hemicontinuity is defined as semicontinuity of the relation fun (x : α) (s : Set β) ↦ IsOpen s ∧ (f x ∩ s).Nonempty. So, f is lower hemicontinuous if, for any open set s, if f x intersects s, then so does f x' for all x' sufficiently close to x. Upper hemicontinuity is defined as semicontinuity of the relation fun (x : α) (s : Set β) ↦ s ∈ 𝓝ˢ (f x). So, f is upper hemicontinuous if any neighborhood of (the set) f x is also a neighborhood of f x' for x' sufficiently close to x. As a final note, sometimes one considers metric upper hemicontinuity, which is yet another concept that can be unified under this framework (although not included in this PR), which is semicontinuity under the relation fun x s ↦ ∃ δ > 0, Metric.thickening (f x) δ ⊆ s. In this PR, we also provide some basic lemmas about upper and lower hemicontinuity which characterize it in terms of preimages, analogous to some characterizations of upper and lower semicontinuity. One very common example of an upper hemicontinuous function is spectrum 𝕜 : A → Set 𝕜, where A is a Banach 𝕜-algebra. This fact will be established in a follow-up PR. The structure of this PR is as follows:

1. Create a new folder / file Topology/Semicontinuity/Defs.lean which contains the new Semicontinuous predicate. In addition, this file provides the boilerplate and definitions of LowerSemicontinuous, UpperSemicontinuous, LowerHemicontinuous and UpperHemicontinuous.
2. The remaining material in Topology/Semicontinuous.lean is moved to Topology/Semicontinuity/Basic.lean (and so the former file is deleted).
3. Some fundamental results about hemicontinuity are added in Topology/Semicontinuity/Hemicontinuity.lean. As a final note, in #maths > Semicontinuity definition for non-linear orders it was suggested that lower semicontinuity be redefined:

-- current definition
def LowerSemicontinuous (f : α → β) := ∀ x y, y < f x → ∀ᶠ x' in 𝓝 x, y < f x'
-- definition proposed in the Zulip thread, equivalent in the linear order case
def LowerSemicontinuous (f : α → β) := ∀ x y, (∃ᶠ x' in 𝓝 x, f x' ≤ y) → f x ≤ y

This change is compatible with the changes made in this PR (there is an example in the source emphasizing this), but this is not implemented here.