Theorems · Definition · probability
PMF.support
{α : Type u_1} → PMF α → Set αThe support of a PMF is the set where it is nonzero.
- Cited by
- 58 results in Mathlib
- Foundations
- Depth 122 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setstatement · cited by 53,352
- Function.supportproof · cited by 610
- PMFstatement and proof · cited by 127
Cited by60
Results whose statement or proof uses this declaration.
- PMF.bindOnSupportstatement and proof · cited by 11
- PMF.filterstatement and proof · cited by 6
- PMF.apply_eq_zero_iffstatement · cited by 3
- PMF.mem_support_iffstatement · cited by 3
- PMF.support_bindstatement and proof · cited by 3
- PMF.support_purestatement · cited by 3
- PMF.toMeasure_apply_eq_toOuterMeasureproof · cited by 3
- PMF.restrict_toMeasure_supportstatement · cited by 2
- PMF.support_countablestatement · cited by 2
- PMF.toOuterMeasure_apply_inter_supportstatement · cited by 2
- PMF.toOuterMeasure_monostatement and proof · cited by 2
- PMF.apply_pos_iffstatement · cited by 1