Theorems · Theorem · probability
SimpleGraph.binomialRandom_zero
∀ (V : Type u_1) [Countable V], SimpleGraph.binomialRandom V 0 = MeasureTheory.Measure.dirac ⊥
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 285 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Countable
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- MeasureTheory.Measurestatement · cited by 10,939
- Set.Elemstatement · cited by 7,166
- Bot.botstatement and proof · cited by 4,720
- SimpleGraphstatement · cited by 3,072
- Compl.complproof · cited by 2,925
- MeasureTheory.Measure.mapproof · cited by 858
- Countablestatement and proof · cited by 633
- unitIntervalstatement · cited by 607
- MeasureTheory.Measure.diracstatement and proof · cited by 210
- SimpleGraph.fromEdgeSetproof · cited by 43
- Sym2.diagSetproof · cited by 41
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.