Commit 2026-02-17 16:40 d5358ace

View on Github →

feat: binomial random graphs (#31364) From LeanCamCombi and formal-conjectures

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Constructions/SimpleGraph.lean

added theorem SimpleGraph.measurableEmbedding_edgeSet

added theorem SimpleGraph.measurable_adj

added theorem SimpleGraph.measurable_edgeSet

added theorem SimpleGraph.measurable_fromEdgeSet

added theorem SimpleGraph.measurable_iff_adj

Created Mathlib/Probability/Combinatorics/BinomialRandomGraph/Defs.lean

added theorem SimpleGraph.binomialRandom_apply'

added theorem SimpleGraph.binomialRandom_apply

added theorem SimpleGraph.binomialRandom_eq_map

added theorem SimpleGraph.binomialRandom_one

added theorem SimpleGraph.binomialRandom_singleton

added theorem SimpleGraph.binomialRandom_zero

Created Mathlib/Probability/Combinatorics/README.md