Documentation

TauCeti.Data.Set.Graph

The function defined by a functional graph #

A set G ⊆ X × Y with injective first projection defines a function on Prod.fst '' G. Set.InjOn.graphValue names that function without extending it outside its domain and without requiring Y to be nonempty. Its values are characterized by membership in G.

The construction uses the inverse of Set.BijOn.equiv for the first projection. In measurable spaces, this description allows Lusin–Souslin to prove measurability of the resulting function.

source
noncomputable def Set.InjOn.graphValue {X : Type u_1} {Y : Type u_2} {G : Set (X × Y)} (hG : InjOn Prod.fst G) (x : ↑(Prod.fst '' G)) :
Y

The function on the domain of a graph with injective first projection. No value outside Prod.fst '' G is chosen.

Instances For
    source
    @[simp]
    theorem Set.InjOn.graphValue_mem {X : Type u_1} {Y : Type u_2} {G : Set (X × Y)} (hG : InjOn Prod.fst G) (x : ↑(Prod.fst '' G)) :
    (↑x, hG.graphValue x) ∈ G

    Every value of the function defined by a functional graph belongs to that graph.

    source
    theorem Set.InjOn.graphValue_eq_of_mem {X : Type u_1} {Y : Type u_2} {G : Set (X × Y)} (hG : InjOn Prod.fst G) {x : X} {y : Y} (h : (x, y) ∈ G) :
    hG.graphValue ⟨x, ⋯⟩ = y

    A point of a functional graph determines the value of its associated function.

    source
    @[simp]
    theorem Set.InjOn.graphValue_eq_iff {X : Type u_1} {Y : Type u_2} {G : Set (X × Y)} (hG : InjOn Prod.fst G) (x : ↑(Prod.fst '' G)) (y : Y) :
    hG.graphValue x = y ↔ (↑x, y) ∈ G

    The value of the function defined by a functional graph is uniquely characterized by membership in that graph.

    source
    @[simp]
    theorem Set.InjOn.graphValue_graphOn {X : Type u_1} {Y : Type u_2} {s : Set X} {f : X → Y} (x : ↑(Prod.fst '' graphOn f s)) :
    ⋯.graphValue x = f ↑x

    Evaluating the function defined by a graph of an existing function recovers that function.

    source
    @[simp]
    theorem Set.InjOn.range_prodMk_graphValue {X : Type u_1} {Y : Type u_2} {G : Set (X × Y)} (hG : InjOn Prod.fst G) :
    (range fun (x : ↑(Prod.fst '' G)) => (↑x, hG.graphValue x)) = G

    The graph is exactly the range of its domain parametrization.

    source
    theorem Set.InjOn.eq_graphValue {X : Type u_1} {Y : Type u_2} {G : Set (X × Y)} (hG : InjOn Prod.fst G) {f : ↑(Prod.fst '' G) → Y} (hf : ∀ (x : ↑(Prod.fst '' G)), (↑x, f x) ∈ G) :
    f = hG.graphValue

    Any function on the domain whose values lie in the graph equals the graph's function.