Pi

📁 Source: Mathlib/Data/Finset/Pi.lean

Statistics

Metric	Count
Definitions `cons`, `empty`, `pi`, `piDiag`, `restrict`, `restrict₂`	6
Theorems `cons_injective`, `cons_ne`, `cons_same`, `card_piDiag`, `dependsOn_restrict`, `mem_pi`, `mem_piDiag`, `piCongrLeft_comp_restrict`, `pi_const_singleton`, `pi_disjoint_of_disjoint`, `pi_empty`, `pi_eq_empty`, `pi_insert`, `pi_nonempty`, `pi_nonempty_of_forall_nonempty`, `pi_singletons`, `pi_subset`, `pi_val`, `restrict_def`, `restrict_preimage`, `restrict_preimage_univ`, `restrict₂_comp_restrict`, `restrict₂_comp_restrict₂`, `restrict₂_def`, `restrict₂_preimage`, `piCongrLeft_comp_restrict`	26
Total	32

Finset

Definitions

Name	Category	Theorems
`pi` 📖	CompOp	18 math math: `card_pi`, `univ_pi_univ`, `inf_sup`, `prod_univ_pi`, `pi_const_singleton`, `sup_inf`, `pi_nonempty`, `pi_empty`, `pi_subset`, `mem_pi`, `pi_disjoint_of_disjoint`, `sum_univ_pi`, `pi_val`, `prod_sum`, `pi_nonempty_of_forall_nonempty`, `pi_eq_empty`, `pi_singletons`, `pi_insert`
`piDiag` 📖	CompOp	4 math math: `card_piDiag`, `mem_piDiag`, `piDiag_subset_piFinset`, `piFinset_filter_const`
`restrict` 📖	CompOp	26 math math: `Function.restrict_updateFinset`, `continuous_restrict_apply`, `measurable_restrict`, `MeasureTheory.lintegral_restrict_infinitePi`, `ProbabilityTheory.IsGaussianProcess.hasGaussianLaw`, `piCongrLeft_comp_restrict`, `ProbabilityTheory.iIndepFun_iff_finset`, `continuous_restrict`, `restrict₂_comp_restrict`, `ProbabilityTheory.isProjectiveMeasureFamily_map_restrict`, `restrict_preimage_univ`, `Function.updateFinset_restrict`, `ProbabilityTheory.identDistrib_iff_forall_finset_identDistrib`, `dependsOn_restrict`, `Function.restrict_updateFinset_of_subset`, `MeasureTheory.mem_cylinder`, `Set.piCongrLeft_comp_restrict`, `ProbabilityTheory.map_eq_iff_forall_finset_map_restrict_eq`, `ProbabilityTheory.isProjectiveLimit_map`, `MeasureTheory.Measure.infinitePiNat_map_restrict`, `measurable_restrict_apply`, `ProbabilityTheory.map_restrict_eq_of_forall_ae_eq`, `restrict_def`, `MeasureTheory.Measure.infinitePi_map_restrict`, `MeasureTheory.integral_restrict_infinitePi`, `restrict_comp_piCongrLeft`
`restrict₂` 📖	CompOp	22 math math: `IocProdIoc_preimage`, `MeasureTheory.inter_cylinder`, `measurable_restrict₂`, `restrict₂_preimage`, `MeasureTheory.cylinder_eq_cylinder_union`, `MeasureTheory.union_cylinder`, `MeasurableEquiv.coe_IicProdIoc_symm`, `continuous_restrict₂`, `MeasureTheory.disjoint_cylinder_iff`, `restrict₂_comp_restrict`, `Function.restrict_updateFinset_of_subset`, `restrict₂_def`, `IicProdIoc_preimage`, `MeasureTheory.eq_of_cylinder_eq_of_subset`, `MeasureTheory.partialTraj_const_restrict₂`, `IicProdIoc_comp_restrict₂`, `measurable_restrict₂_apply`, `ProbabilityTheory.Kernel.lmarginalPartialTraj_eq_lintegral_map`, `ProbabilityTheory.Kernel.partialTraj_eq_prod`, `continuous_restrict₂_apply`, `restrict₂_comp_IicProdIoc`, `restrict₂_comp_restrict₂`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_piDiag` 📖	mathematical	—	`card` `piDiag`	—	`piDiag.eq_1` `card_image_of_injective` `Function.const_injective`
`dependsOn_restrict` 📖	mathematical	—	`DependsOn` `restrict` `SetLike.coe` `Finset` `instSetLike`	—	`Set.dependsOn_restrict`
`mem_pi` 📖	mathematical	—	`Finset` `instMembership` `pi`	—	`Multiset.mem_pi`
`mem_piDiag` 📖	mathematical	—	`Finset` `instMembership` `piDiag`	—	`mem_image`
`piCongrLeft_comp_restrict` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.piCongrLeft` `Finset` `SetLike.instMembership` `instSetLike` `equivToSet` `restrict` `Set.restrict` `SetLike.coe`	—	—
`pi_const_singleton` 📖	mathematical	—	`pi` `Finset` `instSingleton`	—	`pi_singletons`
`pi_disjoint_of_disjoint` 📖	mathematical	`Finset` `instMembership` `Disjoint` `partialOrder` `instOrderBot`	`pi`	—	`disjoint_iff_ne` `mem_pi`
`pi_empty` 📖	mathematical	—	`pi` `Finset` `instEmptyCollection` `instSingleton` `Pi.empty`	—	—
`pi_eq_empty` 📖	mathematical	—	`pi` `Finset` `instEmptyCollection` `instMembership`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₁` `Mathlib.Tactic.Push.not_and_eq` `pi_nonempty`
`pi_insert` 📖	mathematical	`Finset` `instMembership`	`pi` `instInsert` `biUnion` `decidableEqPiFinset` `image` `Pi.cons`	—	`eq_of_veq` `Multiset.Nodup.dedup` `nodup` `Multiset.pi_cons` `Multiset.Nodup.map` `Multiset.Pi.cons_injective` `insert_val_of_notMem`
`pi_nonempty` 📖	mathematical	—	`Nonempty` `pi`	—	—
`pi_nonempty_of_forall_nonempty` 📖	mathematical	`Nonempty`	`pi`	—	`pi_nonempty`
`pi_singletons` 📖	mathematical	—	`pi` `Finset` `instSingleton`	—	—
`pi_subset` 📖	mathematical	`Finset` `instHasSubset`	`pi`	—	`mem_pi`
`pi_val` 📖	mathematical	—	`val` `pi` `Multiset.pi`	—	—
`restrict_def` 📖	mathematical	—	`restrict` `Finset` `SetLike.instMembership` `instSetLike`	—	—
`restrict_preimage` 📖	mathematical	—	`Set.preimage` `Set.restrict` `Set.pi` `Set.Elem` `Set` `Set.instMembership` `SetLike.coe` `Finset` `instSetLike` `image` `Set.univ`	—	—
`restrict_preimage_univ` 📖	mathematical	—	`Set.preimage` `restrict` `Set.pi` `Finset` `SetLike.instMembership` `instSetLike` `Set.univ` `SetLike.coe` `Set` `instMembership`	—	`Set.ext`
`restrict₂_comp_restrict` 📖	mathematical	`Finset` `instHasSubset`	`restrict₂` `restrict`	—	—
`restrict₂_comp_restrict₂` 📖	mathematical	`Finset` `instHasSubset`	`restrict₂` `HasSubset.Subset.trans` `instIsTransSubset`	—	—
`restrict₂_def` 📖	mathematical	`Finset` `instHasSubset`	`restrict₂` `SetLike.instMembership` `instSetLike`	—	—
`restrict₂_preimage` 📖	mathematical	`Finset` `instHasSubset`	`Set.preimage` `restrict₂` `Set.pi` `SetLike.instMembership` `instSetLike` `Set.univ` `Set` `instMembership`	—	`Set.ext` `Set.mem_univ`

Finset.Pi

Definitions

Name	Category	Theorems
`cons` 📖	CompOp	4 math math: `cons_injective`, `cons_ne`, `cons_same`, `Finset.pi_insert`
`empty` 📖	CompOp	1 math math: `Finset.pi_empty`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cons_injective` 📖	mathematical	`Finset` `Finset.instMembership`	`cons`	—	`Multiset.Pi.cons_injective`
`cons_ne` 📖	mathematical	`Finset` `Finset.instMembership` `Finset.instInsert`	`cons` `Finset.mem_insert`	—	`Multiset.Pi.cons_ne`
`cons_same` 📖	mathematical	`Finset` `Finset.instMembership` `Finset.instInsert`	`cons`	—	`Multiset.Pi.cons_same`

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`piCongrLeft_comp_restrict` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.piCongrLeft` `Elem` `SetLike.coe` `Finset` `Finset.instSetLike` `SetLike.instMembership` `Equiv.symm` `Finset.equivToSet` `restrict` `Finset.restrict`	—	—

---

← Back to Index