SetBernoulli

📁 Source: Mathlib/Probability/Distributions/SetBernoulli.lean

Statistics

Metric	Count
Definitions IsSetBernoulli, setBernoulli, «termSetBer(_,_)»»)	3
Theorems ae_subset, instIsProbabilityMeasureSetSetBernoulli, isSetBernoulli_congr, setBernoulli_ae_subset, setBernoulli_apply, setBernoulli_apply', setBernoulli_eq_map, setBernoulli_one, setBernoulli_singleton, setBernoulli_zero	10
Total	13

ProbabilityTheory

Definitions

Name	Category	Theorems
IsSetBernoulli 📖	MathDef	1 math math: isSetBernoulli_congr
setBernoulli 📖	CompOp	8 math math: setBernoulli_one, setBernoulli_singleton, setBernoulli_apply', setBernoulli_zero, instIsProbabilityMeasureSetSetBernoulli, setBernoulli_ae_subset, setBernoulli_apply, setBernoulli_eq_map
«termSetBer(_,_)» 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsProbabilityMeasureSetSetBernoulli 📖	mathematical	—	MeasureTheory.IsProbabilityMeasure Set Set.instMeasurableSpace setBernoulli	—	MeasurableEmbedding.isProbabilityMeasure_comap MeasureTheory.Measure.instIsProbabilityMeasureForallInfinitePi MeasureTheory.instIsProbabilityMeasureHAddMeasureHSMulNNRealToNNRealSymm MeasureTheory.Measure.dirac.isProbabilityMeasure MeasurableEquiv.measurableEmbedding Filter.Eventually.of_forall MeasureTheory.Measure.instOuterMeasureClass
isSetBernoulli_congr 📖	mathematical	Filter.EventuallyEq Set MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	IsSetBernoulli	—	MeasureTheory.Measure.instOuterMeasureClass hasLaw_congr
setBernoulli_ae_subset 📖	mathematical	—	Filter.Eventually Set Set.instHasSubset MeasureTheory.ae MeasureTheory.Measure Set.instMeasurableSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass setBernoulli	—	MeasureTheory.Measure.instOuterMeasureClass Set.setOf_exists Set.inter_empty MeasureTheory.measure_empty IsScalarTower.right Set.inter_univ setBernoulli_apply' Set.ext MeasureTheory.Measure.infinitePi_cylinder MeasureTheory.instIsProbabilityMeasureHAddMeasureHSMulNNRealToNNRealSymm MeasureTheory.Measure.dirac.isProbabilityMeasure Pi.instMeasurableSingletonClass Subtype.countable Prop.instMeasurableSingletonClass MeasureTheory.Measure.pi_singleton MeasureTheory.Add.sigmaFinite MeasureTheory.SMul.sigmaFinite MeasureTheory.Measure.dirac.instSigmaFinite Finset.prod_congr Finset.univ_unique MeasureTheory.Measure.dirac_apply' Set.indicator_singleton Set.indicator_of_notMem smul_zero add_zero Finset.prod_singleton Pi.single_eq_of_ne
setBernoulli_apply 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set Set.instMeasurableSpace ENNReal MeasureTheory.Measure.instFunLike setBernoulli MeasurableSpace.pi Prop.instMeasurableSpace MeasureTheory.Measure.infinitePi MeasureTheory.Measure.instAdd NNReal MeasureTheory.Measure.instSMul Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right unitInterval.toNNReal MeasureTheory.Measure.dirac Set.instMembership unitInterval.symm Set.image	—	MeasurableEmbedding.comap_apply MeasurableEquiv.measurableEmbedding
setBernoulli_apply' 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set Set.instMeasurableSpace ENNReal MeasureTheory.Measure.instFunLike setBernoulli MeasurableSpace.pi Prop.instMeasurableSpace MeasureTheory.Measure.infinitePi MeasureTheory.Measure.instAdd NNReal MeasureTheory.Measure.instSMul Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right unitInterval.toNNReal MeasureTheory.Measure.dirac Set.instMembership unitInterval.symm Set.preimage setOf	—	MeasurableEquiv.comap_apply
setBernoulli_eq_map 📖	mathematical	—	setBernoulli MeasureTheory.Measure.map Set MeasurableSpace.pi Prop.instMeasurableSpace Set.instMeasurableSpace setOf MeasureTheory.Measure.infinitePi MeasureTheory.Measure MeasureTheory.Measure.instAdd NNReal MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right unitInterval.toNNReal MeasureTheory.Measure.dirac Set.instMembership unitInterval.symm	—	MeasurableEquiv.comap_symm
setBernoulli_one 📖	mathematical	—	setBernoulli Set.Elem Real unitInterval Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing MeasureTheory.Measure.dirac Set Set.instMeasurableSpace	—	Real.instIsOrderedRing IsScalarTower.right setBernoulli_eq_map one_smul unitInterval.symm_one zero_smul add_zero MeasureTheory.Measure.infinitePi_dirac MeasureTheory.Measure.map_dirac
setBernoulli_singleton 📖	mathematical	Set Set.instHasSubset	DFunLike.coe MeasureTheory.Measure Set.instMeasurableSpace ENNReal MeasureTheory.Measure.instFunLike setBernoulli Set.instSingletonSet Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero ENNReal.ofNNReal unitInterval.toNNReal Set.ncard unitInterval.symm Set.instSDiff	—	CanLift.prf Set.instCanLiftFinsetCoeFinite IsScalarTower.right setBernoulli_apply Set.image_singleton MeasureTheory.Measure.infinitePi_singleton MeasureTheory.instIsProbabilityMeasureHAddMeasureHSMulNNRealToNNRealSymm MeasureTheory.Measure.dirac.isProbabilityMeasure Prop.instMeasurableSingletonClass MeasureTheory.Measure.dirac_apply' smul_ite smul_zero mul_one tprod_eq_prod SummationFilter.instLeAtTopUnconditional unitInterval.toNNReal_add_toNNReal_symm Finset.prod_congr ite_add_ite add_zero zero_add Finset.prod_ite Finset.prod_const Finset.coe_filter Set.inter_eq_right Set.inter_comm Set.diff_eq_compl_inter
setBernoulli_zero 📖	mathematical	—	setBernoulli Set.Elem Real unitInterval Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing MeasureTheory.Measure.dirac Set Set.instMeasurableSpace Set.instEmptyCollection	—	Real.instIsOrderedRing IsScalarTower.right setBernoulli_eq_map zero_smul unitInterval.symm_zero one_smul zero_add MeasureTheory.Measure.infinitePi_dirac MeasureTheory.Measure.map_dirac

ProbabilityTheory.IsSetBernoulli

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_subset 📖	mathematical	ProbabilityTheory.IsSetBernoulli	Filter.Eventually Set Set.instHasSubset MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.HasLaw.ae_iff Measurable.subset measurable_id' measurable_const ProbabilityTheory.setBernoulli_ae_subset

---

← Back to Index