FactorsThrough

📁 Source: Mathlib/MeasureTheory/Function/FactorsThrough.lean

Statistics

Metric	Count
Definitions FactorsThrough, FactorsThrough	2
Theorems dependsOn_of_piFinset, dependsOn_of_piLE, exists_eq_measurable_comp, factorsThrough, dependsOn_of_piFinset, dependsOn_of_piLE, exists_eq_measurable_comp, factorsThrough	8
Total	10

DirichletCharacter

Definitions

Name	Category	Theorems
FactorsThrough 📖	MathDef	8 math math: FactorsThrough.same_level, factorsThrough_of_gaussSum_ne_zero, changeLevel_factorsThrough, mem_conductorSet_iff, factorsThrough_gcd, factorsThrough_iff_ker_unitsMap, factorsThrough_conductor, factorsThrough_one_iff

Function

Definitions

Name	Category	Theorems
FactorsThrough 📖	MathDef	10 math math: PolynomialLaw.factorsThrough_toFunLifted_π, factorsThrough_of_pullbackCondition, Topology.IsQuotientMap.liftEquiv_symm_apply_coe, MeasureTheory.StronglyMeasurable.factorsThrough, Measurable.factorsThrough, FactorsThrough.rfl, factorsThrough_iff, Topology.IsQuotientMap.liftEquiv_apply, dependsOn_iff_factorsThrough, Injective.factorsThrough

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dependsOn_of_piFinset 📖	mathematical	Measurable MeasureTheory.Filtration.seq Finset PartialOrder.toPreorder Finset.partialOrder MeasurableSpace.pi MeasureTheory.Filtration.piFinset	DependsOn SetLike.coe Finset.instSetLike	—	dependsOn_iff_factorsThrough factorsThrough
dependsOn_of_piLE 📖	mathematical	Measurable MeasureTheory.Filtration.seq MeasurableSpace.pi MeasureTheory.Filtration.piLE	DependsOn Set.Iic	—	dependsOn_iff_factorsThrough factorsThrough
exists_eq_measurable_comp 📖	—	Measurable MeasurableSpace.comap	—	—	MeasureTheory.StronglyMeasurable.exists_eq_measurable_comp PolishSpace.toIsCompletelyMetrizableSpace UpgradedStandardBorel.toPolishSpace stronglyMeasurable TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace TopologicalSpace.IsCompletelyMetrizableSpace.MetrizableSpace PolishSpace.toSecondCountableTopology BorelSpace.opensMeasurable UpgradedStandardBorel.toBorelSpace MeasureTheory.StronglyMeasurable.measurable
factorsThrough 📖	mathematical	Measurable MeasurableSpace.comap	Function.FactorsThrough	—	Set.eq_of_mem_singleton MeasurableSingletonClass.measurableSet_singleton Set.mem_preimage Set.mem_singleton_iff

MeasureTheory.StronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dependsOn_of_piFinset 📖	mathematical	MeasureTheory.StronglyMeasurable MeasureTheory.Filtration.seq Finset PartialOrder.toPreorder Finset.partialOrder MeasurableSpace.pi MeasureTheory.Filtration.piFinset	DependsOn SetLike.coe Finset.instSetLike	—	dependsOn_iff_factorsThrough factorsThrough
dependsOn_of_piLE 📖	mathematical	MeasureTheory.StronglyMeasurable MeasureTheory.Filtration.seq MeasurableSpace.pi MeasureTheory.Filtration.piLE	DependsOn Set.Iic	—	dependsOn_iff_factorsThrough factorsThrough
exists_eq_measurable_comp 📖	—	MeasureTheory.StronglyMeasurable MeasurableSpace.comap	—	—	induction' MeasureTheory.stronglyMeasurable_const piecewise Set.piecewise_comp limUnder instCountableNat instIsCountablyGenerated_atTop OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace PseudoEMetricSpace.pseudoMetrizableSpace Filter.Tendsto.limUnder_eq TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.IsCompletelyMetrizableSpace.MetrizableSpace Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat
factorsThrough 📖	mathematical	MeasureTheory.StronglyMeasurable MeasurableSpace.comap	Function.FactorsThrough	—	Measurable.factorsThrough OpensMeasurableSpace.toMeasurableSingletonClass BorelSpace.opensMeasurable measurable

---

← Back to Index