Sigma-algebra on simple graphs

In this file, we pull back the sigma-algebra on V → V → Prop to a sigma-algebra on SimpleGraph V and prove that common operations are measurable.

@[instance_reducible]

instance SimpleGraph.instMeasurableSpace {V : Type u_1} : MeasurableSpace (SimpleGraph V)

Equations

• SimpleGraph.instMeasurableSpace = MeasurableSpace.comap SimpleGraph.Adj inferInstance

theorem SimpleGraph.measurable_iff_adj {V : Type u_1} {Ω : Type u_2} {m : MeasurableSpace Ω} {G : Ω → SimpleGraph V} : Measurable G ↔ ∀ (u v : V), Measurable fun (ω : Ω) => (G ω).Adj u v

A simple graph-valued map is measurable iff all induced adjacency maps are measurable.

theorem SimpleGraph.measurable_adj {V : Type u_1} : Measurable Adj

theorem SimpleGraph.measurable_edgeSet {V : Type u_1} : Measurable edgeSet

@[simp]

theorem SimpleGraph.measurable_fromEdgeSet {V : Type u_1} : Measurable fromEdgeSet

theorem SimpleGraph.measurableEmbedding_edgeSet {V : Type u_1} [Countable V] : MeasurableEmbedding edgeSet