Documentation Verification Report

Prod

📁 Source: Mathlib/MeasureTheory/MeasurableSpace/Prod.lean

Statistics

MetricCount
Definitions0
TheoremsprodMap, prodMk_left, prodMk_right, comap_prodMap, comap_prodMk, generateFrom_eq_prod, generateFrom_prod, generateFrom_prod_eq, isPiSystem_prod, measurableEmbedding_prodMk_left, measurableEmbedding_prod_mk_right
11
Total11

MeasurableEmbedding

Theorems

NameKindAssumesProvesValidatesDepends On
prodMap 📖mathematicalMeasurableEmbeddingProd.instMeasurableSpace—iff_comap_eq
Function.Injective.prodMap
injective
Prod.instMeasurableSpace.eq_1
MeasurableSpace.comap_prodMap
comap_eq
Set.range_prodMap
MeasurableSet.prod
measurableSet_range
prodMk_left 📖mathematicalMeasurableEmbeddingProd.instMeasurableSpace—injective
Measurable.prodMk
measurable_const
measurable
Set.ext
MeasurableSet.prod
MeasurableSet.singleton
measurableSet_image
prodMk_right 📖mathematicalMeasurableEmbeddingProd.instMeasurableSpace—comp
MeasurableEquiv.measurableEmbedding
prodMk_left

MeasurableSpace

Theorems

NameKindAssumesProvesValidatesDepends On
comap_prodMap 📖mathematical—comap
prod		—comap_sup
comap_comp
comap_prodMk 📖mathematical—comap
prod
MeasurableSpace
SemilatticeSup.toMax
Lattice.toSemilatticeSup
ConditionallyCompleteLattice.toLattice
CompleteLattice.toConditionallyCompleteLattice
instCompleteLattice		—comap_sup
comap_comp

(root)

Theorems

NameKindAssumesProvesValidatesDepends On
generateFrom_eq_prod 📖mathematicalMeasurableSpace.generateFrom
IsCountablySpanning		Set.image2
Set
SProd.sprod
Set.instSProd
Prod.instMeasurableSpace		—generateFrom_prod_eq
generateFrom_prod 📖mathematical—MeasurableSpace.generateFrom
Set.image2
Set
SProd.sprod
Set.instSProd
setOf
MeasurableSet
Prod.instMeasurableSpace		—generateFrom_eq_prod
MeasurableSpace.generateFrom_measurableSet
isCountablySpanning_measurableSet
generateFrom_prod_eq 📖mathematicalIsCountablySpanningProd.instMeasurableSpace
MeasurableSpace.generateFrom
Set.image2
Set
SProd.sprod
Set.instSProd		—le_antisymm
sup_le
MeasurableSpace.comap_generateFrom
MeasurableSpace.generateFrom_le
Set.prod_univ
Set.prod_iUnion
MeasurableSet.iUnion
instCountableNat
MeasurableSpace.measurableSet_generateFrom
Set.univ_prod
Set.iUnion_prod_const
Set.mem_image2_of_mem
Set.prod_eq
MeasurableSet.inter
measurable_fst
measurable_snd
isPiSystem_prod 📖mathematical—IsPiSystem
Set.image2
Set
SProd.sprod
Set.instSProd
setOf
MeasurableSet		—IsPiSystem.prod
MeasurableSpace.isPiSystem_measurableSet
measurableEmbedding_prodMk_left 📖mathematical—MeasurableEmbedding
Prod.instMeasurableSpace		—MeasurableEmbedding.prodMk_left
MeasurableEmbedding.id
measurableEmbedding_prod_mk_right 📖mathematical—MeasurableEmbedding
Prod.instMeasurableSpace		—MeasurableEmbedding.prodMk_right
MeasurableEmbedding.id

---

← Back to Index