Borel graphs with singleton vertical sections

A functional Borel graph — a Borel G ⊆ X × Y with at most one y above each x — has a Borel domain, and the partial function it names is Borel measurable.

Both facts are Lusin–Souslin (Gao, Invariant Descriptive Set Theory, CRC Press, 2009, Theorem 1.3.1), which Mathlib supplies; this file packages the argument so consumers never restate it. Nothing here is model-theoretic.

The results

• measurableSet_domain — the domain Prod.fst '' G is Borel. Proved directly, with no subtype: MeasurableSet.image_of_measurable_injOn asks for InjOn, and InjOn Prod.fst G is exactly the functionality hypothesis.
• measurableEmbedding_proj — the projection ↥G → X is a measurable embedding. Restricting the projection to ↥G turns injOn_fst into the global injectivity required by Measurable.measurableEmbedding.
• equivDomain — hence a measurable equivalence ↥G ≃ᵐ ↥domain, whose inverse is measurable by construction.
• value, measurable_value, value_mem, value_eq_of_mem — the induced partial function on the domain, measurable, and identified: a measurable-but-unspecified map would be unusable, so the two specifications are part of the interface rather than an afterthought.

Scope

Only the canonical subtype-domain value map is built. Totalized forms — X → Option Y, or a junk-valued X → Y — are derivable from it and are deliberately deferred until a consumer needs one; building all three now would fix an interface no caller has yet exercised.

structure BorelFunctionalGraph {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (G : Set (X × Y)) : Prop

A Borel graph whose vertical sections are singletons or empty: it names a partial function.

• measurableSet_graph : MeasurableSet G

  The graph is Borel.

• functional {x : X} {y z : Y} : (x, y) ∈ G → (x, z) ∈ G → y = z

  At most one point lies above each first coordinate.

def BorelFunctionalGraph.domain {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {G : Set (X × Y)} (_h : BorelFunctionalGraph G) : Set X

The domain: the first coordinates covered by the graph.

Depends only on G — the evidence is taken so that h.domain reads naturally at use sites.

Equations

• _h.domain = Prod.fst '' G

theorem BorelFunctionalGraph.mem_domain_iff {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {G : Set (X × Y)} (h : BorelFunctionalGraph G) {x : X} : x ∈ h.domain ↔ ∃ (y : Y), (x, y) ∈ G

theorem BorelFunctionalGraph.injOn_fst {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {G : Set (X × Y)} (h : BorelFunctionalGraph G) : Set.InjOn Prod.fst G

Functionality, as injectivity of the projection on G. This is the exact hypothesis MeasurableSet.image_of_measurable_injOn consumes.

theorem BorelFunctionalGraph.measurableSet_domain {X : Type u} {Y : Type v} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {G : Set (X × Y)} (h : BorelFunctionalGraph G) : MeasurableSet h.domain

The domain is Borel (Lusin–Souslin).

The subtype layer

Restricting the projection to ↥G turns injOn_fst into the global injectivity required by Measurable.measurableEmbedding.

def BorelFunctionalGraph.proj {X : Type u} {Y : Type v} (G : Set (X × Y)) : ↑G → X

The projection of the graph onto its first coordinate.

Equations

• BorelFunctionalGraph.proj G p = (↑p).1

theorem BorelFunctionalGraph.injective_proj {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {G : Set (X × Y)} (h : BorelFunctionalGraph G) : Function.Injective (proj G)

theorem BorelFunctionalGraph.measurable_proj {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {G : Set (X × Y)} : Measurable (proj G)

theorem BorelFunctionalGraph.range_proj {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {G : Set (X × Y)} (h : BorelFunctionalGraph G) : Set.range (proj G) = h.domain

theorem BorelFunctionalGraph.measurableEmbedding_proj {X : Type u} {Y : Type v} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {G : Set (X × Y)} (h : BorelFunctionalGraph G) : MeasurableEmbedding (proj G)

The projection is a measurable embedding (Lusin–Souslin).

noncomputable def BorelFunctionalGraph.equivDomain {X : Type u} {Y : Type v} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {G : Set (X × Y)} (h : BorelFunctionalGraph G) : ↑G ≃ᵐ ↑h.domain

The graph is measurably equivalent to its domain. In particular the inverse of the projection is measurable — the point of the whole construction.

Built explicitly with a transparent forward map, so coe_equivDomain holds by rfl; measurability of the inverse comes from MeasurableEmbedding.measurable_rangeSplitting.

Equations

• One or more equations did not get rendered due to their size.

theorem BorelFunctionalGraph.coe_equivDomain {X : Type u} {Y : Type v} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {G : Set (X × Y)} (h : BorelFunctionalGraph G) (p : ↑G) : ↑(h.equivDomain p) = proj G p

The forward map is the projection — true by construction, and what identifies value.

The value map

value alone would be unusable: a measurable map with no stated relation to G identifies nothing. value_mem and value_eq_of_mem are therefore part of the interface — the first says the selected value is the one the graph names, the second is uniqueness in the form callers actually apply.

noncomputable def BorelFunctionalGraph.value {X : Type u} {Y : Type v} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {G : Set (X × Y)} (h : BorelFunctionalGraph G) (x : ↑h.domain) : Y

The partial function named by the graph, on its domain.

Equations

• h.value x = (↑(h.equivDomain.symm x)).2

theorem BorelFunctionalGraph.value_mem {X : Type u} {Y : Type v} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {G : Set (X × Y)} (h : BorelFunctionalGraph G) (x : ↑h.domain) : (↑x, h.value x) ∈ G

The selected value is the one the graph names.

theorem BorelFunctionalGraph.value_eq_of_mem {X : Type u} {Y : Type v} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {G : Set (X × Y)} (h : BorelFunctionalGraph G) {x : ↑h.domain} {y : Y} (hy : (↑x, y) ∈ G) : h.value x = y

Uniqueness, in the form callers apply: any value the graph names at a domain point is the selected one.

theorem BorelFunctionalGraph.measurable_value {X : Type u} {Y : Type v} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {G : Set (X × Y)} (h : BorelFunctionalGraph G) : Measurable h.value

The value map is measurable.