Closure properties and the cardinality bound of analytic sets

Mathlib's analytic sets (MeasureTheory.AnalyticSet) are closed under countable unions and intersections, continuous images and continuous preimages from Polish spaces. This file adds the finite and relational closure properties used to manipulate analytic relations and analytic equivalence relations: binary intersections and unions, intersections with Borel sets, products and their images under jointly continuous binary maps, continuous preimages taken inside an analytic set, off-diagonals, projections, and images and preimages of an analytic set under an analytic relation R : SetRel α β. In a Hausdorff space the last of these show that the saturation Quotient.mk E ⁻¹' (Quotient.mk E '' A) of an analytic set A under an equivalence relation E with analytic graph is analytic, and so is the neighbourhood {x | ∃ y ∈ A, (x, y) ∈ G ∨ (y, x) ∈ G} of A under an analytic relation G, which is (G ∪ G.inv).preimage A and is analytic by (hG.union hG.relInv).relPreimage hA. Combined with Lusin separation (MeasureTheory.AnalyticSet.measurablySeparable), these are the inputs of separation arguments that alternate between Borel separators and their saturations or neighbourhoods.

As the continuous image of the Baire space ℕ → ℕ, an analytic set has at most continuum many points (MeasureTheory.AnalyticSet.mk_le_continuum).

Binary intersections are proved in a Hausdorff ambient space, as Mathlib's MeasureTheory.AnalyticSet.iInter is. Intersection with a Borel set needs no separation axiom: an analytic set is the continuous image of a Polish space, and the preimage of a Borel set there is Borel, hence analytic.

Main results

• MeasureTheory.AnalyticSet.inter, MeasureTheory.AnalyticSet.union: binary intersections (in a Hausdorff space) and unions of analytic sets are analytic.
• MeasureTheory.AnalyticSet.inter_measurableSet: the intersection of an analytic set with a Borel set is analytic.
• MeasureTheory.AnalyticSet.prod, MeasureTheory.AnalyticSet.offDiag: products of analytic sets, and off-diagonals of analytic sets in a Hausdorff space, are analytic.
• MeasureTheory.AnalyticSet.image2: the image of a product of analytic sets under a jointly continuous binary map is analytic.
• MeasureTheory.AnalyticSet.inter_preimage: within an analytic set, the preimage of an analytic subset of a Hausdorff space under a continuous map is analytic.
• MeasureTheory.AnalyticSet.relImage, MeasureTheory.AnalyticSet.relPreimage: the image and preimage of an analytic set under an analytic relation are analytic.
• MeasureTheory.AnalyticSet.relImage_measurableSet, MeasureTheory.AnalyticSet.relPreimage_measurableSet: the image and preimage of a Borel set under an analytic relation are analytic, with no separation axiom.
• MeasureTheory.AnalyticSet.preimage_image_quotientMk, MeasureTheory.AnalyticSet.preimage_image_quotientMk_measurableSet: the saturation of an analytic set (in a Hausdorff space) or of a Borel set under an equivalence relation with analytic graph is analytic.
• MeasureTheory.AnalyticSet.mk_le_continuum: an analytic set has at most 𝔠 points.

References

• A. S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer, 1995, Proposition 14.4 (closure properties of analytic sets).
• inter, inter_measurableSet, prod and offDiag are adapted from InfinitaryLogic/Descriptive/AnalyticClosure.lean in cameronfreer/infinitary-logic (Apache-2.0); the proofs of inter and prod follow it, and inter_measurableSet is stated there for Polish spaces only.

theorem MeasureTheory.AnalyticSet.inter {α : Type u_1} [TopologicalSpace α] [T2Space α] {s t : Set α} (hs : AnalyticSet s) (ht : AnalyticSet t) : AnalyticSet (s ∩ t)

The intersection of two analytic sets in a Hausdorff space is analytic.

theorem MeasureTheory.AnalyticSet.union {α : Type u_1} [TopologicalSpace α] {s t : Set α} (hs : AnalyticSet s) (ht : AnalyticSet t) : AnalyticSet (s ∪ t)

The union of two analytic sets is analytic.

theorem MeasureTheory.AnalyticSet.inter_measurableSet {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] {s t : Set α} (hs : AnalyticSet s) (ht : MeasurableSet t) : AnalyticSet (s ∩ t)

The intersection of an analytic set with a Borel set is analytic, in any topological space with its Borel σ-algebra.

theorem MeasureTheory.AnalyticSet.prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set β} (hs : AnalyticSet s) (ht : AnalyticSet t) : AnalyticSet (s ×ˢ t)

The product of two analytic sets is analytic.

theorem MeasureTheory.AnalyticSet.image2 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {γ : Type u_3} [TopologicalSpace γ] {f : α → β → γ} (hf : Continuous (Function.uncurry f)) {s : Set α} {t : Set β} (hs : AnalyticSet s) (ht : AnalyticSet t) : AnalyticSet (Set.image2 f s t)

The image of a product of analytic sets under a jointly continuous binary map is analytic.

theorem MeasureTheory.AnalyticSet.inter_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T2Space β] {s : Set α} (hs : AnalyticSet s) {f : α → β} (hf : Continuous f) {t : Set β} (ht : AnalyticSet t) : AnalyticSet (s ∩ f ⁻¹' t)

The points of an analytic set at which a continuous map into a Hausdorff space takes values in an analytic set form an analytic set.

theorem MeasureTheory.AnalyticSet.offDiag {α : Type u_1} [TopologicalSpace α] [T2Space α] {s : Set α} (hs : AnalyticSet s) : AnalyticSet s.offDiag

The set of pairs of distinct points of an analytic set in a Hausdorff space is analytic.

theorem MeasureTheory.AnalyticSet.image_fst {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set (α × β)} (hs : AnalyticSet s) : AnalyticSet (Prod.fst '' s)

The first projection of an analytic subset of a product is analytic.

theorem MeasureTheory.AnalyticSet.image_snd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set (α × β)} (hs : AnalyticSet s) : AnalyticSet (Prod.snd '' s)

The second projection of an analytic subset of a product is analytic.

theorem MeasureTheory.AnalyticSet.relInv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {R : SetRel α β} (hR : AnalyticSet R) : AnalyticSet R.inv

The inverse of an analytic relation is analytic.

theorem MeasureTheory.AnalyticSet.relImage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T2Space α] {R : SetRel α β} (hR : AnalyticSet R) {s : Set α} (hs : AnalyticSet s) : AnalyticSet (R.image s)

The image of an analytic set under an analytic relation is analytic, when the domain is Hausdorff.

theorem MeasureTheory.AnalyticSet.relPreimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T2Space β] {R : SetRel α β} (hR : AnalyticSet R) {t : Set β} (ht : AnalyticSet t) : AnalyticSet (R.preimage t)

The preimage of an analytic set under an analytic relation is analytic, when the codomain is Hausdorff.

theorem MeasureTheory.AnalyticSet.relPreimage_measurableSet {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] {R : SetRel α β} (hR : AnalyticSet R) {t : Set β} (ht : MeasurableSet t) : AnalyticSet (R.preimage t)

The preimage of a Borel set under an analytic relation is analytic. No separation axiom is needed: the preimage is the first projection of the intersection of the relation with a Borel set.

theorem MeasureTheory.AnalyticSet.relImage_measurableSet {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [MeasurableSpace α] [BorelSpace α] {R : SetRel α β} (hR : AnalyticSet R) {s : Set α} (hs : MeasurableSet s) : AnalyticSet (R.image s)

The image of a Borel set under an analytic relation is analytic.

theorem MeasureTheory.AnalyticSet.preimage_image_quotientMk {α : Type u_1} [TopologicalSpace α] [T2Space α] {E : Setoid α} (hE : AnalyticSet {p : α × α | E p.1 p.2}) {s : Set α} (hs : AnalyticSet s) : AnalyticSet (Quotient.mk E ⁻¹' Quotient.mk E '' s)

The saturation of an analytic set under an equivalence relation with analytic graph, in a Hausdorff space, is analytic.

theorem MeasureTheory.AnalyticSet.preimage_image_quotientMk_measurableSet {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Setoid α} (hE : AnalyticSet {p : α × α | E p.1 p.2}) {s : Set α} (hs : MeasurableSet s) : AnalyticSet (Quotient.mk E ⁻¹' Quotient.mk E '' s)

The saturation of a Borel set under an equivalence relation with analytic graph is analytic, with no separation axiom.

theorem MeasureTheory.AnalyticSet.mk_le_continuum {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : AnalyticSet s) : Cardinal.mk ↑s ≤ Cardinal.continuum

An analytic set has at most continuum many points.