Theorem: ErdosRenyi.meas (LeanCamCombi/ErdosRenyi/Basic.lean)

State before:
α : Type u_1
Ω : Type u_2
inst✝⁵ : MeasurableSpace Ω
G : Ω → SimpleGraph α
H : SimpleGraph α
inst✝⁴ : (ω : Ω) → DecidableRel (G ω).Adj
p : ℝ≥0
μ : Measure Ω
inst✝³ : IsProbabilityMeasure μ
hG : ErdosRenyi G p μ
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel H.Adj
⊢ μ {ω | G ω = H} = ↑p ^ H.edgeFinset.card * (1 - ↑p) ^ (Fintype.card (Sym2 α) - H.edgeFinset.card)
Tactic:
simpa using hG.meas H.edgeFinset
State after:
no goals