TProd

📁 Source: Mathlib/Data/Prod/TProd.lean

Statistics

Metric	Count
Definitions TProd, elim, elim', instInhabited, mk, piEquivTProd, tprod	7
Theorems elim_mk, elim_of_mem, elim_of_ne, elim_self, ext, ext_iff, fst_mk, mk_elim, snd_mk, elim_preimage_pi, mk_preimage_tprod	11
Total	18

List

Definitions

Name	Category	Theorems
TProd 📖	CompOp	11 math math: MeasureTheory.Measure.sigmaFinite_tprod, measurable_tProd_elim', MeasurableSet.tProd, measurable_tProd_elim, measurable_tProd_mk, MeasurableEquiv.piMeasurableEquivTProd_apply, MeasureTheory.Measure.tprod_cons, MeasureTheory.Measure.tprod_tprod, Set.elim_preimage_pi, MeasurableEquiv.piMeasurableEquivTProd_symm_apply, Set.mk_preimage_tprod

List.TProd

Definitions

Name	Category	Theorems
elim 📖	CompOp	6 math math: elim_of_mem, elim_self, measurable_tProd_elim, elim_mk, elim_of_ne, ext_iff
elim' 📖	CompOp	4 math math: mk_elim, measurable_tProd_elim', Set.elim_preimage_pi, MeasurableEquiv.piMeasurableEquivTProd_symm_apply
instInhabited 📖	CompOp	—
mk 📖	CompOp	—
piEquivTProd 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
elim_mk 📖	mathematical	—	elim	—	elim_self elim_of_ne
elim_of_mem 📖	mathematical	—	elim	—	elim_of_ne List.Nodup.notMem
elim_of_ne 📖	mathematical	—	elim	—	—
elim_self 📖	mathematical	—	elim	—	—
ext 📖	—	elim	—	—	elim_self elim_of_mem
ext_iff 📖	mathematical	—	elim	—	ext
fst_mk 📖	—	—	—	—	—
mk_elim 📖	mathematical	—	elim'	—	ext
snd_mk 📖	—	—	—	—	—

Set

Definitions

Name	Category	Theorems
tprod 📖	CompOp	4 math math: MeasurableSet.tProd, MeasureTheory.Measure.tprod_tprod, elim_preimage_pi, mk_preimage_tprod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
elim_preimage_pi 📖	mathematical	—	preimage List.TProd List.TProd.elim' pi univ tprod	—	ext mk_preimage_tprod preimage_preimage List.TProd.mk_elim
mk_preimage_tprod 📖	mathematical	—	preimage List.TProd tprod pi setOf	—	empty_pi ext tprod.eq_2 mem_preimage mem_pi prodMk_mem_set_prod_eq

---

← Back to Index