Indep

📁 Source: Mathlib/Probability/Independence/Kernel/Indep.lean

Statistics

Metric	Count
Definitions `Indep`, `Indep`, `Indep`, `Indep`, `IndepSet`, `IndepSets`, `iIndep`, `iIndepSet`, `iIndepSets`	9
Theorems `indepSet_of_measurableSet`, `indepSets`, `measure_inter_eq_mul`, `bInter`, `bUnion`, `biUnion`, `iInter`, `iUnion`, `indep`, `indep'`, `indepSet_of_mem`, `indep_aux`, `inter`, `union`, `union_iff`, `ae_isProbabilityMeasure`, `iIndepSets`, `iIndepSets'`, `indep`, `meas_biInter`, `meas_iInter`, `of_precomp`, `of_subsingleton`, `precomp`, `indep_generateFrom_le`, `indep_generateFrom_le_nat`, `indep_generateFrom_lt`, `indep_generateFrom_of_disjoint`, `meas_biInter`, `of_precomp`, `precomp`, `iIndepSet_congr`, `iIndepSet_iff_iIndepSets_singleton`, `iIndepSet_iff_meas_biInter`, `iIndepSet_precomp_of_bijective`, `iIndepSet_zero_right`, `ae_isProbabilityMeasure`, `iIndep`, `iIndepSet_of_mem`, `indepSets`, `meas_biInter`, `meas_iInter`, `of_precomp`, `of_subsingleton`, `piiUnionInter_of_notMem`, `precomp`, `iIndepSets_congr`, `iIndepSets_precomp_of_bijective`, `iIndepSets_singleton_iff`, `iIndepSets_zero_right`, `iIndep_comap_mem_iff`, `iIndep_congr`, `iIndep_of_iIndep_of_le`, `iIndep_precomp_of_bijective`, `iIndep_zero_right`, `indepSet_congr`, `indepSet_empty_left`, `indepSet_empty_right`, `indepSet_iff_indepSets_singleton`, `indepSet_iff_measure_inter_eq_mul`, `indepSet_zero_left`, `indepSet_zero_right`, `indepSets_congr`, `indepSets_of_indepSets_of_le_left`, `indepSets_of_indepSets_of_le_right`, `indepSets_piiUnionInter_of_disjoint`, `indepSets_singleton_iff`, `indepSets_zero_left`, `indepSets_zero_right`, `indep_bot_left`, `indep_bot_right`, `indep_congr`, `indep_iSup_of_antitone`, `indep_iSup_of_directed_le`, `indep_iSup_of_disjoint`, `indep_iSup_of_monotone`, `indep_iff_forall_indepSet`, `indep_of_indep_of_le_left`, `indep_of_indep_of_le_right`, `indep_zero_left`, `indep_zero_right`	81
Total	90

IndepMatroid

Definitions

Name	Category	Theorems
`Indep` 📖	MathDef	16 math math: `ofFinset_indep`, `ofFinite_indep`, `matroid_IsBase`, `ofBddAugment_indep`, `ofFinitary_indep`, `Matroid.restrictIndepMatroid_Indep`, `indep_empty`, `matroid_Indep`, `ofBdd_indep`, `indep_aug`, `ofFinitaryCardAugment_indep`, `indep_subset`, `indep_maximal`, `Matroid.dualIndepMatroid_Indep`, `ofFinset_indep'`, `matroid_indep_iff`

Matroid

Definitions

Name	Category	Theorems
`Indep` 📖	MathDef	160 math math: `Indep.exists_insert_of_encard_lt`, `Indep.mem_fundCircuit_iff`, `Dep.not_indep`, `restrictSubtype_indep_iff`, `removeLoops_indep_eq`, `ext_indep_iff`, `IsNonloop.contractElem_indep_iff`, `IsBasis'.insert_not_indep`, `isBasis_iff`, `indep_iff_delete_of_disjoint`, `Indep.diff`, `disjointSigma_indep_iff`, `indep_iff_forall_closure_diff_ne`, `Indep.indep_isRestriction`, `isBasis_iff_indep_encard_eq_of_finite`, `uniqueBaseOn_indep_iff'`, `AlgebraicIndependent.matroid_indep_iff`, `Finitary.indep_of_forall_finite`, `le_eRk_iff`, `IsNonloop.closure_eq_closure_iff_eq_or_dep`, `Indep.exists_bijOn_of_map`, `IsBasis.contract_indep_iff`, `Indep.map`, `Indep.exists_eq_image_of_mapSetEmbedding`, `insert_indep_iff`, `cRank_eq_iSup_cardinalMk_indep`, `IsBase.exists_insert_of_ssubset`, `sum'_indep_iff`, `loopyOn_indep_iff`, `dual_coindep_iff`, `finitary_iff`, `comapOn_indep_iff`, `deleteElem_indep_iff`, `restrict_eq_restrict_iff`, `restrict_dep_iff`, `Indep.mapEmbedding`, `restrictIndepMatroid_Indep`, `ext_iff`, `indep_iff_forall_subset_not_isCircuit`, `isBasis_iff_indep_subset_closure`, `Indep.diff_indep_contract_of_subset`, `indep_iff`, `isBasis_self_iff_indep`, `comap_indep_iff`, `Indep.union_indep_iff_forall_notMem_closure_left`, `dual_indep_iff_exists'`, `mapEmbedding_indep_iff`, `indep_iff_not_dep`, `Indep.subset`, `mapSetEmbedding_indep_iff'`, `Indep.insert_indep_iff`, `freeOn_indep`, `indep_iff_forall_finite_subset_indep`, `Indep.union_indep_iff_contract_indep`, `Indep.notMem_closure_iff`, `isBasis_iff'`, `IsBasis.contract_indep_iff_of_disjoint`, `indep_iff_forall_closure_ssubset_of_ssubset`, `comap_indep_iff_of_injOn`, `restrictSubtype_inter_indep_iff`, `sum_indep_iff`, `Indep.inter_left`, `indep_iff_eRk_eq_encard_of_finite`, `comap_dep_iff`, `IsBasis'.indep`, `emptyOn_indep_iff`, `maximality`, `singleton_not_indep`, `coloops_indep`, `empty_indep`, `exists_mem_finite_closure_of_mem_closure`, `restrict_eq_freeOn_iff`, `mapSetEmbedding_indep_iff`, `setOf_indep_eq`, `isCircuit_iff_dep_forall_diff_singleton_indep`, `Coindep.indep`, `map_indep_iff`, `indep_iff_forall_notMem_closure_diff'`, `Indep.exists_insert_of_not_isBase`, `IsCircuit.not_indep`, `Indep.exists_insert_of_not_isBasis`, `IndepMatroid.matroid_Indep`, `indep_singleton`, `ground_indep_iff_eq_freeOn`, `Indep.indep_restrict_of_subset`, `Indep.eq_union_image_of_disjointSum`, `restrictSubtype_indep_iff_of_subset`, `Indep.of_isMinor`, `indep_of_forall_finite_subset_indep`, `IsBasis.contract_indep_diff_iff`, `dual_indep_iff_exists`, `Indep.of_isRestriction`, `Indep.notMem_closure_iff_of_notMem`, `isBasis_iff_maximal`, `Indep.of_contract`, `indep_iff_eRk_eq_encard`, `Indep.contract_indep_iff`, `IsColoop.insert_indep_of_indep`, `diff_coloops_indep_iff`, `indep_or_dep`, `isCircuit_iff_forall_ssubset`, `isBase_iff_indep_closure_eq`, `Indep.of_restrict`, `Indep.inter_right`, `ground_indep_iff_isBase`, `copy_Indep`, `mapEquiv_indep_iff`, `copyIndep_Indep`, `Indep.exists_insert_of_not_maximal`, `not_dep_iff`, `uniqueBaseOn_indep_iff`, `isCircuit_iff_minimal_not_indep`, `Indep.indep_delete_of_disjoint`, `IsCircuit.diff_singleton_indep`, `map_image_indep_iff`, `Indep.indep_insert_diff_of_mem_closure`, `copyBase_Indep`, `restrict_indep_iff`, `eq_freeOn_iff`, `freeOn_indep_iff`, `isBasis'_iff_indep_encard_eq_of_finite`, `Indep.insert_diff_indep_iff`, `isBasis_union_iff_indep_closure`, `not_indep_iff`, `indep_iff_forall_notMem_closure_diff`, `IsBasis.indep`, `Indep.union_indep_iff_forall_notMem_closure_right`, `IsBase.indep`, `isBase_iff_maximal_indep`, `sigma_indep_iff`, `IsCircuit.minimal_not_indep`, `IsRkFinite.indep_of_encard_le_eRk`, `Indep.augment_finset`, `ext_iff_indep`, `delete_indep_iff`, `subsingleton_indep`, `IsRestriction.indep_iff`, `mapSetEquiv_indep_iff`, `isBasis_iff_indep_closure`, `union_indep_iff_indep_of_subset_coloops`, `disjointSum_indep_iff`, `IsBasis'.contract_indep_diff_iff`, `union_coloops_indep_iff`, `Indep.augment`, `IsBasis'.contract_indep_iff`, `diff_indep_iff_indep_of_subset_coloops`, `Indep.of_delete`, `IsCircuit.ssubset_indep`, `indep_iff'`, `existsMaximalSubsetProperty_indep`, `exists_subset_finite_closure_of_subset_closure`, `dep_iff`, `IsLoop.not_indep_of_mem`, `indep_iff_forall_subset_not_isCircuit'`, `coindep_def`, `indep_of_not_dep`, `IsNonloop.indep`, `IndepMatroid.matroid_indep_iff`, `setOf_dep_eq`, `Indep.insert_indep_iff_of_notMem`

ProbabilityTheory

Definitions

Name	Category	Theorems
`Indep` 📖	MathDef	34 math math: `IndepSets.indep'`, `indep_iSup_of_monotone`, `indep_limsup_atTop_self`, `IndepFun_iff_Indep`, `indep_biSup_limsup`, `indep_iSup_of_directed_le`, `Indep_iff`, `IndepSet_iff_Indep`, `indep_comap_of_bcf`, `Indep.symm`, `iIndepFun.indep_comap_natural_of_lt`, `iIndepSet.indep_generateFrom_le`, `indep_comap_pi_of_bcf`, `indep_iSup_limsup`, `iIndep.indep`, `iIndepSet.indep_generateFrom_lt`, `indep_iSup_directed_limsup`, `indep_comap_process_of_bcf`, `indep_iff_forall_indepSet`, `indep_comap_process_of_prod_bcf`, `indep_limsup_atBot_self`, `indep_iSup_of_antitone`, `indep_bot_right`, `Indep_iff_IndepSets`, `indep_bot_left`, `indep_of_indep_of_le_right`, `iIndepSet.indep_generateFrom_le_nat`, `indep_biSup_compl`, `indep_comap_pi_of_prod_bcf`, `indep_of_indep_of_le_left`, `IndepSets.indep`, `iIndepSet.indep_generateFrom_of_disjoint`, `indep_iSup_of_disjoint`, `indep_limsup_self`

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
`Indep` 📖	MathDef	28 math math: `iIndepSet.indep_generateFrom_of_disjoint`, `Indep.congr`, `iIndepSet.indep_generateFrom_le_nat`, `indep_zero_right`, `indep_iSup_directed_limsup`, `indep_limsup_atBot_self`, `iIndepSet.indep_generateFrom_le`, `indep_iff_forall_indepSet`, `indep_iSup_limsup`, `iIndepSet.indep_generateFrom_lt`, `indep_of_indep_of_le_left`, `indep_limsup_self`, `Indep.symm`, `indep_iSup_of_directed_le`, `indep_iSup_of_monotone`, `indep_biSup_limsup`, `iIndep.indep`, `indep_limsup_atTop_self`, `indep_iSup_of_antitone`, `indep_congr`, `IndepSets.indep`, `indep_bot_left`, `indep_of_indep_of_le_right`, `IndepSets.indep'`, `indep_bot_right`, `indep_zero_left`, `indep_biSup_compl`, `indep_iSup_of_disjoint`
`IndepSet` 📖	MathDef	12 math math: `indepSet.congr`, `indepSet_zero_left`, `indep_iff_forall_indepSet`, `indepSet_iff_measure_inter_eq_mul`, `IndepSets.indepSet_of_mem`, `indepSet_empty_left`, `indepSet_zero_right`, `indepSet_congr`, `indepSet_empty_right`, `indepSet_iff_indepSets_singleton`, `indepFun_iff_indepSet_preimage`, `Indep.indepSet_of_measurableSet`
`IndepSets` 📖	MathDef	21 math math: `IndepSets.symm`, `IndepSets.congr`, `IndepSets.biUnion`, `iIndepSets.indepSets`, `indepSets_piiUnionInter_of_disjoint`, `indepSets_zero_left`, `IndepSets.iInter`, `IndepSets.bInter`, `indepSets_of_indepSets_of_le_right`, `IndepSets.iUnion`, `IndepSets.union_iff`, `indepSets_zero_right`, `Indep.indepSets`, `indepSets_of_indepSets_of_le_left`, `indepSet_iff_indepSets_singleton`, `iIndepSets.piiUnionInter_of_notMem`, `IndepSets.union`, `IndepSets.bUnion`, `indepSets_congr`, `indepSets_singleton_iff`, `IndepSets.inter`
`iIndep` 📖	MathDef	11 math math: `iIndep_of_iIndep_of_le`, `iIndep.of_subsingleton`, `iIndepFun.iIndep`, `iIndepSets.iIndep`, `iIndep.congr`, `iIndep_congr`, `iIndep_comap_mem_iff`, `iIndep_precomp_of_bijective`, `iIndep.of_precomp`, `iIndep_zero_right`, `iIndep.precomp`
`iIndepSet` 📖	MathDef	10 math math: `iIndepSet_iff_meas_biInter`, `iIndepSet.congr`, `iIndepSets.iIndepSet_of_mem`, `iIndepSet_precomp_of_bijective`, `iIndep_comap_mem_iff`, `iIndepSet.of_precomp`, `iIndepSet.precomp`, `iIndepSet_iff_iIndepSets_singleton`, `iIndepSet_congr`, `iIndepSet_zero_right`
`iIndepSets` 📖	MathDef	11 math math: `iIndep.iIndepSets'`, `iIndepSets.congr`, `iIndepSets_congr`, `iIndepSets.precomp`, `iIndepSets_precomp_of_bijective`, `iIndepSets_zero_right`, `iIndep.iIndepSets`, `iIndepSets_singleton_iff`, `iIndepSets.of_subsingleton`, `iIndepSet_iff_iIndepSets_singleton`, `iIndepSets.of_precomp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iIndepSet_congr` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.Measure` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `instFunLike`	`iIndepSet`	—	`MeasureTheory.Measure.instOuterMeasureClass` `iIndep_congr`
`iIndepSet_iff_iIndepSets_singleton` 📖	mathematical	`MeasurableSet`	`iIndepSet` `iIndepSets` `Set` `Set.instSingletonSet`	—	`iIndep.iIndepSets` `iIndepSets.iIndep` `MeasurableSpace.generateFrom_le` `IsPiSystem.singleton`
`iIndepSet_iff_meas_biInter` 📖	mathematical	`MeasurableSet`	`iIndepSet` `Filter.Eventually` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `ProbabilityTheory.Kernel` `instFunLike` `Set.iInter` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `iIndepSet_iff_iIndepSets_singleton` `iIndepSets_singleton_iff`
`iIndepSet_precomp_of_bijective` 📖	mathematical	`Function.Bijective`	`iIndepSet` `Set`	—	`iIndepSet.of_precomp` `Function.Bijective.surjective` `iIndepSet.precomp` `Function.Bijective.injective`
`iIndepSet_zero_right` 📖	mathematical	—	`iIndepSet` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero`	—	`MeasurableSpace.generateFrom_singleton`
`iIndepSets_congr` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.Measure` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `instFunLike`	`iIndepSets`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.mp_mem` `Filter.univ_mem'` `Finset.prod_congr`
`iIndepSets_precomp_of_bijective` 📖	mathematical	`Function.Bijective`	`iIndepSets` `Set`	—	`iIndepSets.of_precomp` `Function.Bijective.surjective` `iIndepSets.precomp` `Function.Bijective.injective`
`iIndepSets_singleton_iff` 📖	mathematical	—	`iIndepSets` `Set` `Set.instSingletonSet` `Filter.Eventually` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `ProbabilityTheory.Kernel` `instFunLike` `Set.iInter` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.mp_mem` `Filter.univ_mem'` `Finset.prod_congr` `Set.iInter₂_congr`
`iIndepSets_zero_right` 📖	mathematical	—	`iIndepSets` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_zero`
`iIndep_comap_mem_iff` 📖	mathematical	—	`iIndep` `MeasurableSpace.comap` `Set` `Set.instMembership` `Top.top` `MeasurableSpace` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `MeasurableSpace.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `iIndepSet`	—	—
`iIndep_congr` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.Measure` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `instFunLike`	`iIndep`	—	`MeasureTheory.Measure.instOuterMeasureClass` `iIndepSets_congr`
`iIndep_of_iIndep_of_le` 📖	mathematical	`iIndep` `MeasurableSpace` `MeasurableSpace.instLE`	`iIndep`	—	—
`iIndep_precomp_of_bijective` 📖	mathematical	`Function.Bijective`	`iIndep` `MeasurableSpace`	—	`iIndep.of_precomp` `Function.Bijective.surjective` `iIndep.precomp` `Function.Bijective.injective`
`iIndep_zero_right` 📖	mathematical	—	`iIndep` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero`	—	—
`indepSet_congr` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.Measure` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `instFunLike`	`IndepSet`	—	`MeasureTheory.Measure.instOuterMeasureClass` `indep_congr`
`indepSet_empty_left` 📖	mathematical	—	`IndepSet` `Set` `Set.instEmptyCollection`	—	`Indep.symm` `indepSet_empty_right`
`indepSet_empty_right` 📖	mathematical	—	`IndepSet` `Set` `Set.instEmptyCollection`	—	`MeasurableSpace.generateFrom_singleton_empty` `indep_bot_right`
`indepSet_iff_indepSets_singleton` 📖	mathematical	`MeasurableSet`	`IndepSet` `IndepSets` `Set` `Set.instSingletonSet`	—	`Indep.indepSets` `IndepSets.indep` `MeasurableSpace.generateFrom_le` `Set.mem_singleton_iff` `IsPiSystem.singleton`
`indepSet_iff_measure_inter_eq_mul` 📖	mathematical	`MeasurableSet`	`IndepSet` `Filter.Eventually` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `ProbabilityTheory.Kernel` `instFunLike` `Set.instInter` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `indepSet_iff_indepSets_singleton` `indepSets_singleton_iff`
`indepSet_zero_left` 📖	mathematical	—	`IndepSet` `ProbabilityTheory.Kernel` `instZero`	—	`MeasurableSpace.generateFrom_singleton`
`indepSet_zero_right` 📖	mathematical	—	`IndepSet` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero`	—	`MeasurableSpace.generateFrom_singleton`
`indepSets_congr` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.Measure` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `instFunLike`	`IndepSets`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.mp_mem` `Filter.univ_mem'`
`indepSets_of_indepSets_of_le_left` 📖	mathematical	`IndepSets` `Set` `Set.instHasSubset`	`IndepSets`	—	`Set.mem_of_subset_of_mem`
`indepSets_of_indepSets_of_le_right` 📖	mathematical	`IndepSets` `Set` `Set.instHasSubset`	`IndepSets`	—	`Set.mem_of_subset_of_mem`
`indepSets_piiUnionInter_of_disjoint` 📖	mathematical	`iIndepSets` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`IndepSets` `piiUnionInter`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Finset.mem_union` `Set.disjoint_left` `Set.inter_univ` `Set.disjoint_right` `Set.univ_inter` `Set.ext` `Set.iInter_congr_Prop` `Filter.mp_mem` `Filter.univ_mem'` `iIndepSets.ae_isProbabilityMeasure` `Set.disjoint_iff_forall_ne` `mul_one` `one_mul` `MeasureTheory.IsProbabilityMeasure.measure_univ` `Finset.prod_congr` `Finset.prod_mul_distrib` `Finset.prod_ite_mem` `Finset.union_inter_cancel_left` `Finset.union_inter_cancel_right`
`indepSets_singleton_iff` 📖	mathematical	—	`IndepSets` `Set` `Set.instSingletonSet` `Filter.Eventually` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `ProbabilityTheory.Kernel` `instFunLike` `Set.instInter` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Set.mem_singleton_iff`
`indepSets_zero_left` 📖	mathematical	—	`IndepSets` `ProbabilityTheory.Kernel` `instZero`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MulZeroClass.mul_zero`
`indepSets_zero_right` 📖	mathematical	—	`IndepSets` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_zero`
`indep_bot_left` 📖	mathematical	—	`Indep` `Bot.bot` `MeasurableSpace` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `MeasurableSpace.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`Indep.symm` `indep_bot_right`
`indep_bot_right` 📖	mathematical	—	`Indep` `Bot.bot` `MeasurableSpace` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `MeasurableSpace.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`MeasureTheory.Measure.instOuterMeasureClass` `ProbabilityTheory.eq_zero_or_isMarkovKernel` `MulZeroClass.mul_zero` `Filter.Eventually.of_forall` `MeasurableSpace.measurableSet_bot_iff` `Set.mem_setOf_eq` `Set.inter_empty` `MeasureTheory.measure_empty` `Set.inter_univ` `MeasureTheory.IsProbabilityMeasure.measure_univ` `ProbabilityTheory.IsMarkovKernel.is_probability_measure'` `mul_one`
`indep_congr` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.Measure` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `instFunLike`	`Indep`	—	`MeasureTheory.Measure.instOuterMeasureClass` `indepSets_congr`
`indep_iSup_of_antitone` 📖	mathematical	`Indep` `MeasurableSpace` `MeasurableSpace.instLE` `Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `MeasurableSpace.instPartialOrder`	`Indep` `iSup` `MeasurableSpace` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `MeasurableSpace.instCompleteLattice`	—	`indep_iSup_of_directed_le` `Antitone.directed_le` `SemilatticeInf.instIsCodirectedOrder`
`indep_iSup_of_directed_le` 📖	mathematical	`Indep` `MeasurableSpace` `MeasurableSpace.instLE` `Directed`	`Indep` `iSup` `MeasurableSpace` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `MeasurableSpace.instCompleteLattice`	—	`MeasurableSpace.isPiSystem_measurableSet` `MeasurableSpace.generateFrom_measurableSet` `isPiSystem_iUnion_of_directed_le` `IndepSets.iUnion` `Indep.indepSets` `IndepSets.indep` `iSup_le` `MeasurableSpace.generateFrom_iUnion_measurableSet`
`indep_iSup_of_disjoint` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `iIndep` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`Indep` `iSup` `MeasurableSpace` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `MeasurableSpace.instCompleteLattice` `Set` `Set.instMembership`	—	`eq_or_ne` `MeasureTheory.Measure.instOuterMeasureClass` `exists_ae_eq_isMarkovKernel` `iIndep.ae_isProbabilityMeasure` `Indep.congr` `Filter.EventuallyEq.symm` `IndepSets.indep` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `iSup₂_le` `isPiSystem_piiUnionInter` `MeasurableSpace.isPiSystem_measurableSet` `generateFrom_piiUnionInter_measurableSet` `indepSets_piiUnionInter_of_disjoint` `iIndep.congr`
`indep_iSup_of_monotone` 📖	mathematical	`Indep` `MeasurableSpace` `MeasurableSpace.instLE` `Monotone` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `MeasurableSpace.instPartialOrder`	`Indep` `iSup` `MeasurableSpace` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `MeasurableSpace.instCompleteLattice`	—	`indep_iSup_of_directed_le` `Monotone.directed_le` `SemilatticeSup.instIsDirectedOrder`
`indep_iff_forall_indepSet` 📖	mathematical	—	`Indep` `IndepSet`	—	`Indep.indepSet_of_measurableSet` `MeasurableSpace.measurableSet_generateFrom` `Set.mem_singleton`
`indep_of_indep_of_le_left` 📖	mathematical	`Indep` `MeasurableSpace` `MeasurableSpace.instLE`	`Indep`	—	—
`indep_of_indep_of_le_right` 📖	mathematical	`Indep` `MeasurableSpace` `MeasurableSpace.instLE`	`Indep`	—	—
`indep_zero_left` 📖	mathematical	—	`Indep` `ProbabilityTheory.Kernel` `instZero`	—	—
`indep_zero_right` 📖	mathematical	—	`Indep` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero`	—	—

ProbabilityTheory.Kernel.Indep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`indepSet_of_measurableSet` 📖	mathematical	`ProbabilityTheory.Kernel.Indep` `MeasurableSet`	`ProbabilityTheory.Kernel.IndepSet`	—	`MeasurableSpace.generateFrom_induction` `MeasurableSet.empty` `MeasurableSet.compl` `MeasurableSet.iUnion` `instCountableNat`
`indepSets` 📖	mathematical	`ProbabilityTheory.Kernel.Indep` `MeasurableSpace.generateFrom`	`ProbabilityTheory.Kernel.IndepSets`	—	`MeasurableSpace.measurableSet_generateFrom`

ProbabilityTheory.Kernel.IndepSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measure_inter_eq_mul` 📖	mathematical	`ProbabilityTheory.Kernel.IndepSet`	`Filter.Eventually` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `Set.instInter` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`ProbabilityTheory.Kernel.Indep.indepSets`

ProbabilityTheory.Kernel.IndepSets

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bInter` 📖	mathematical	`Set` `Set.instMembership` `ProbabilityTheory.Kernel.IndepSets`	`ProbabilityTheory.Kernel.IndepSets` `Set.iInter` `Set` `Set.instMembership`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Set.biInter_subset_of_mem`
`bUnion` 📖	mathematical	`ProbabilityTheory.Kernel.IndepSets`	`ProbabilityTheory.Kernel.IndepSets` `Set.iUnion` `Set` `Set.instMembership`	—	`biUnion`
`biUnion` 📖	mathematical	`ProbabilityTheory.Kernel.IndepSets`	`ProbabilityTheory.Kernel.IndepSets` `Set.iUnion` `Set` `Set.instMembership`	—	`MeasureTheory.Measure.instOuterMeasureClass`
`iInter` 📖	mathematical	`ProbabilityTheory.Kernel.IndepSets`	`ProbabilityTheory.Kernel.IndepSets` `Set.iInter` `Set`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Set.mem_iInter`
`iUnion` 📖	mathematical	`ProbabilityTheory.Kernel.IndepSets`	`ProbabilityTheory.Kernel.IndepSets` `Set.iUnion` `Set`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Set.mem_iUnion`
`indep` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `IsPiSystem` `MeasurableSpace.generateFrom` `ProbabilityTheory.Kernel.IndepSets`	`ProbabilityTheory.Kernel.Indep`	—	`ProbabilityTheory.eq_zero_or_isMarkovKernel` `MeasurableSpace.induction_on_inter` `MeasureTheory.Measure.instOuterMeasureClass` `Set.empty_inter` `MeasureTheory.measure_empty` `MulZeroClass.zero_mul` `indep_aux` `MeasurableSpace.measurableSet_generateFrom` `Filter.mp_mem` `Filter.univ_mem'` `Set.inter_comm` `Set.diff_self_inter` `Set.diff_eq_compl_inter` `MeasureTheory.measure_diff` `Set.inter_subset_left` `MeasurableSet.nullMeasurableSet` `MeasurableSet.inter` `MeasureTheory.measure_ne_top` `ProbabilityTheory.IsFiniteKernel.isFiniteMeasure` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `MeasureTheory.measure_compl` `MeasureTheory.IsProbabilityMeasure.measure_univ` `ProbabilityTheory.IsMarkovKernel.is_probability_measure'` `mul_comm` `ENNReal.mul_sub` `mul_one` `MeasureTheory.ae_all_iff` `instCountableNat` `Set.inter_iUnion` `MeasureTheory.measure_iUnion` `Function.onFun.eq_1` `Disjoint.inter_left` `Disjoint.inter_right` `ENNReal.tsum_mul_right`
`indep'` 📖	mathematical	`MeasurableSet` `IsPiSystem` `ProbabilityTheory.Kernel.IndepSets`	`ProbabilityTheory.Kernel.Indep` `MeasurableSpace.generateFrom`	—	`indep` `MeasurableSpace.generateFrom_le`
`indepSet_of_mem` 📖	mathematical	`Set` `Set.instMembership` `MeasurableSet` `ProbabilityTheory.Kernel.IndepSets`	`ProbabilityTheory.Kernel.IndepSet`	—	`MeasureTheory.Measure.instOuterMeasureClass` `ProbabilityTheory.Kernel.indepSet_iff_measure_inter_eq_mul`
`indep_aux` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `IsPiSystem` `MeasurableSpace.generateFrom` `ProbabilityTheory.Kernel.IndepSets` `Set` `Set.instMembership` `MeasurableSet`	`Filter.Eventually` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `Set.instInter` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `ProbabilityTheory.eq_zero_or_isMarkovKernel` `MulZeroClass.mul_zero` `MeasurableSpace.induction_on_inter` `Set.inter_empty` `MeasureTheory.measure_empty` `Filter.mp_mem` `Filter.univ_mem'` `Set.diff_eq` `Set.diff_self_inter` `MeasureTheory.measure_diff` `Set.inter_subset_left` `MeasurableSet.nullMeasurableSet` `MeasurableSet.inter` `MeasureTheory.measure_ne_top` `ProbabilityTheory.IsFiniteKernel.isFiniteMeasure` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `MeasureTheory.measure_compl` `MeasureTheory.IsProbabilityMeasure.measure_univ` `ProbabilityTheory.IsMarkovKernel.is_probability_measure'` `ENNReal.mul_sub` `mul_one` `MeasureTheory.ae_all_iff` `instCountableNat` `Set.inter_iUnion` `MeasureTheory.measure_iUnion` `Pairwise.mono` `Disjoint.inter_right'` `Disjoint.inter_left'` `ENNReal.tsum_mul_left`
`inter` 📖	mathematical	`ProbabilityTheory.Kernel.IndepSets`	`ProbabilityTheory.Kernel.IndepSets` `Set` `Set.instInter`	—	`Set.mem_inter_iff`
`union` 📖	mathematical	`ProbabilityTheory.Kernel.IndepSets`	`ProbabilityTheory.Kernel.IndepSets` `Set` `Set.instUnion`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Set.mem_union`
`union_iff` 📖	mathematical	—	`ProbabilityTheory.Kernel.IndepSets` `Set` `Set.instUnion`	—	`ProbabilityTheory.Kernel.indepSets_of_indepSets_of_le_left` `Set.subset_union_left` `Set.subset_union_right` `union`

ProbabilityTheory.Kernel.iIndep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_isProbabilityMeasure` 📖	mathematical	`ProbabilityTheory.Kernel.iIndep`	`Filter.Eventually` `MeasureTheory.IsProbabilityMeasure` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`ProbabilityTheory.Kernel.iIndepSets.ae_isProbabilityMeasure` `iIndepSets'`
`iIndepSets` 📖	mathematical	`MeasurableSpace.generateFrom` `ProbabilityTheory.Kernel.iIndep`	`ProbabilityTheory.Kernel.iIndepSets`	—	`MeasurableSpace.measurableSet_generateFrom`
`iIndepSets'` 📖	mathematical	`ProbabilityTheory.Kernel.iIndep`	`ProbabilityTheory.Kernel.iIndepSets` `setOf` `Set` `MeasurableSet`	—	—
`indep` 📖	mathematical	`ProbabilityTheory.Kernel.iIndep`	`ProbabilityTheory.Kernel.Indep`	—	`ProbabilityTheory.Kernel.iIndepSets.indepSets`
`meas_biInter` 📖	mathematical	`ProbabilityTheory.Kernel.iIndep` `MeasurableSet`	`Filter.Eventually` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `Set.iInter` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	—
`meas_iInter` 📖	mathematical	`ProbabilityTheory.Kernel.iIndep` `MeasurableSet`	`Filter.Eventually` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `Set.iInter` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `meas_biInter` `Filter.univ_mem'` `Set.iInter_congr_Prop` `Set.iInter_true`
`of_precomp` 📖	mathematical	`ProbabilityTheory.Kernel.iIndep` `MeasurableSpace`	`ProbabilityTheory.Kernel.iIndep`	—	`ProbabilityTheory.Kernel.iIndepSets.of_precomp`
`of_subsingleton` 📖	mathematical	—	`ProbabilityTheory.Kernel.iIndep`	—	—
`precomp` 📖	mathematical	`ProbabilityTheory.Kernel.iIndep`	`ProbabilityTheory.Kernel.iIndep` `MeasurableSpace`	—	`ProbabilityTheory.Kernel.iIndepSets.precomp`

ProbabilityTheory.Kernel.iIndepSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`indep_generateFrom_le` 📖	mathematical	`MeasurableSet` `ProbabilityTheory.Kernel.iIndepSet` `Preorder.toLT`	`ProbabilityTheory.Kernel.Indep` `MeasurableSpace.generateFrom` `Set` `Set.instSingletonSet` `setOf` `Preorder.toLE`	—	`Set.setOf_eq_eq_singleton'` `indep_generateFrom_of_disjoint` `Set.disjoint_singleton_left` `LT.lt.not_ge`
`indep_generateFrom_le_nat` 📖	mathematical	`MeasurableSet` `ProbabilityTheory.Kernel.iIndepSet`	`ProbabilityTheory.Kernel.Indep` `MeasurableSpace.generateFrom` `Set` `Set.instSingletonSet` `setOf`	—	`indep_generateFrom_le`
`indep_generateFrom_lt` 📖	mathematical	`MeasurableSet` `ProbabilityTheory.Kernel.iIndepSet`	`ProbabilityTheory.Kernel.Indep` `MeasurableSpace.generateFrom` `Set` `Set.instSingletonSet` `setOf` `Preorder.toLT`	—	`Set.setOf_eq_eq_singleton'` `indep_generateFrom_of_disjoint` `Set.disjoint_singleton_left` `lt_irrefl`
`indep_generateFrom_of_disjoint` 📖	mathematical	`MeasurableSet` `ProbabilityTheory.Kernel.iIndepSet` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`ProbabilityTheory.Kernel.Indep` `MeasurableSpace.generateFrom` `setOf` `Set` `Set.instMembership`	—	`eq_or_ne` `MeasureTheory.Measure.instOuterMeasureClass` `ProbabilityTheory.Kernel.exists_ae_eq_isMarkovKernel` `ProbabilityTheory.Kernel.iIndep.ae_isProbabilityMeasure` `ProbabilityTheory.Kernel.Indep.congr` `Filter.EventuallyEq.symm` `generateFrom_piiUnionInter_singleton_left` `ProbabilityTheory.Kernel.IndepSets.indep'` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `generateFrom_piiUnionInter_le` `MeasurableSpace.generateFrom_le` `Set.mem_singleton_iff` `MeasurableSpace.measurableSet_generateFrom` `isPiSystem_piiUnionInter` `IsPiSystem.singleton` `ProbabilityTheory.Kernel.indepSets_piiUnionInter_of_disjoint` `ProbabilityTheory.Kernel.iIndep.iIndepSets` `congr`
`meas_biInter` 📖	mathematical	`ProbabilityTheory.Kernel.iIndepSet`	`Filter.Eventually` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `Set.iInter` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`ProbabilityTheory.Kernel.iIndep.iIndepSets`
`of_precomp` 📖	mathematical	`ProbabilityTheory.Kernel.iIndepSet` `Set`	`ProbabilityTheory.Kernel.iIndepSet`	—	`ProbabilityTheory.Kernel.iIndep.of_precomp`
`precomp` 📖	mathematical	`ProbabilityTheory.Kernel.iIndepSet`	`ProbabilityTheory.Kernel.iIndepSet` `Set`	—	`ProbabilityTheory.Kernel.iIndep.precomp`

ProbabilityTheory.Kernel.iIndepSets

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_isProbabilityMeasure` 📖	mathematical	`ProbabilityTheory.Kernel.iIndepSets`	`Filter.Eventually` `MeasureTheory.IsProbabilityMeasure` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `meas_biInter` `instIsEmptyFalse` `Filter.univ_mem'` `Set.iInter_congr_Prop` `Set.iInter_of_empty` `Set.iInter_univ` `Finset.prod_const` `pow_zero`
`iIndep` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `IsPiSystem` `MeasurableSpace.generateFrom` `ProbabilityTheory.Kernel.iIndepSets`	`ProbabilityTheory.Kernel.iIndep`	—	`eq_or_ne` `MeasureTheory.Measure.instOuterMeasureClass` `ProbabilityTheory.Kernel.exists_ae_eq_isMarkovKernel` `ae_isProbabilityMeasure` `ProbabilityTheory.Kernel.iIndep.congr` `Filter.EventuallyEq.symm` `Finset.induction` `instIsEmptyFalse` `Set.iInter_congr_Prop` `Set.iInter_of_empty` `Set.iInter_univ` `MeasureTheory.IsProbabilityMeasure.measure_univ` `ProbabilityTheory.IsMarkovKernel.is_probability_measure'` `isPiSystem_piiUnionInter` `Eq.trans_le` `generateFrom_piiUnionInter_le` `ProbabilityTheory.Kernel.IndepSets.indep` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `piiUnionInter_of_notMem` `congr` `ProbabilityTheory.Kernel.Indep.symm` `Finset.mem_insert_self` `le_generateFrom_piiUnionInter` `Finset.measurableSet_biInter` `Filter.mp_mem` `Filter.univ_mem'` `Finset.set_biInter_insert` `Finset.prod_insert`
`iIndepSet_of_mem` 📖	mathematical	`Set` `Set.instMembership` `MeasurableSet` `ProbabilityTheory.Kernel.iIndepSets`	`ProbabilityTheory.Kernel.iIndepSet`	—	`MeasureTheory.Measure.instOuterMeasureClass` `ProbabilityTheory.Kernel.iIndepSet_iff_meas_biInter` `meas_biInter`
`indepSets` 📖	mathematical	`ProbabilityTheory.Kernel.iIndepSets`	`ProbabilityTheory.Kernel.IndepSets`	—	`Finset.mem_insert` `Finset.mem_singleton` `Finset.set_biInter_insert` `Finset.set_biInter_singleton` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.univ_mem'`
`meas_biInter` 📖	mathematical	`ProbabilityTheory.Kernel.iIndepSets` `Set` `Set.instMembership`	`Filter.Eventually` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `Set.iInter` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	—
`meas_iInter` 📖	mathematical	`ProbabilityTheory.Kernel.iIndepSets` `Set` `Set.instMembership`	`Filter.Eventually` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `Set.iInter` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ` `MeasureTheory.ae` `MeasureTheory.Measure.instOuterMeasureClass`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `meas_biInter` `Filter.univ_mem'` `Set.iInter_congr_Prop` `Set.iInter_true`
`of_precomp` 📖	mathematical	`ProbabilityTheory.Kernel.iIndepSets` `Set`	`ProbabilityTheory.Kernel.iIndepSets`	—	`Function.Surjective.hasRightInverse` `Function.comp_assoc` `Function.RightInverse.comp_eq_id` `precomp` `Function.RightInverse.injective`
`of_subsingleton` 📖	mathematical	—	`ProbabilityTheory.Kernel.iIndepSets`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Set.Subsingleton.eq_empty_or_singleton` `Set.subsingleton_of_subsingleton` `Set.iInter_congr_Prop` `Set.iInter_of_empty` `instIsEmptyFalse` `Set.iInter_univ` `MeasureTheory.IsProbabilityMeasure.measure_univ` `ProbabilityTheory.IsMarkovKernel.is_probability_measure'` `Set.iInter_iInter_eq_left` `Finset.prod_singleton`
`piiUnionInter_of_notMem` 📖	mathematical	`ProbabilityTheory.Kernel.iIndepSets` `Finset` `SetLike.instMembership` `Finset.instSetLike`	`ProbabilityTheory.Kernel.IndepSets` `piiUnionInter` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Finset.mem_insert` `Finset.coe_subset` `Filter.mp_mem` `Filter.univ_mem'` `Finset.set_biInter_insert` `Set.inter_comm` `Finset.prod_insert` `mul_comm`
`precomp` 📖	mathematical	`ProbabilityTheory.Kernel.iIndepSets`	`ProbabilityTheory.Kernel.iIndepSets` `Set`	—	`Function.Injective.extend_apply` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.univ_mem'` `Set.iInter_congr_Prop` `Set.iInter_exists` `Set.biInter_and'` `Set.iInter_iInter_eq_right` `Finset.prod_image` `Function.Injective.injOn` `Finset.prod_congr`

---

← Back to Index