Jacobian

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

Statistics

Metric	Count
Definitions `Jacobian`	1
Theorems `norm_fderiv_sub_le`, `withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul`, `withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul`, `addHaar_image_eq_zero_of_det_fderivWithin_eq_zero`, `addHaar_image_eq_zero_of_det_fderivWithin_eq_zero_aux`, `addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero`, `addHaar_image_le_lintegral_abs_det_fderiv`, `addHaar_image_le_lintegral_abs_det_fderiv_aux1`, `addHaar_image_le_lintegral_abs_det_fderiv_aux2`, `addHaar_image_le_mul_of_det_lt`, `aemeasurable_fderivWithin`, `aemeasurable_ofReal_abs_det_fderivWithin`, `aemeasurable_toNNReal_abs_det_fderivWithin`, `integrableOn_image_iff_integrableOn_abs_det_fderiv_smul`, `integral_image_eq_integral_abs_det_fderiv_smul`, `integral_target_eq_integral_abs_det_fderiv_smul`, `lintegral_abs_det_fderiv_eq_addHaar_image`, `lintegral_abs_det_fderiv_eq_addHaar_image₀`, `lintegral_abs_det_fderiv_le_addHaar_image`, `lintegral_abs_det_fderiv_le_addHaar_image_aux1`, `lintegral_abs_det_fderiv_le_addHaar_image_aux2`, `lintegral_image_eq_lintegral_abs_det_fderiv_mul`, `map_withDensity_abs_det_fderiv_eq_addHaar`, `measurableEmbedding_of_fderivWithin`, `measurable_image_of_fderivWithin`, `mul_le_addHaar_image_of_lt_det`, `nullMeasurable_image_of_fderivWithin`, `restrict_map_withDensity_abs_det_fderiv_eq_addHaar`, `exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt`, `exists_partition_approximatesLinearOn_of_hasFDerivWithinAt`	30
Total	31

ApproximatesLinearOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_fderiv_sub_le` 📖	mathematical	`ApproximatesLinearOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `MeasurableSet` `HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Filter.Eventually` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `ContinuousLinearMap.sub` `Real.instRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `RingHomIsometric.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.ae_restrict_mem` `Besicovitch.ae_tendsto_measure_inter_div` `UniformSpace.secondCountable_of_separable` `EMetric.instIsCountablyGeneratedUniformity` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `FiniteDimensional.proper_real` `Besicovitch.instHasBesicovitchCovering` `MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `Filter.univ_mem'` `ContinuousLinearMap.opNorm_le_bound` `MeasureTheory.Measure.eventually_nonempty_inter_smul_of_density_one` `measurableSet_closedBall` `BorelSpace.opensMeasurable` `LT.lt.ne'` `Metric.measure_closedBall_pos` `MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure` `Metric.mem_nhdsWithin_iff` `Asymptotics.IsLittleO.def` `HasFDerivAtFilter.isLittleO` `nhdsWithin_le_nhds` `eventually_singleton_add_smul_subset` `Metric.isBounded_closedBall` `Metric.ball_mem_nhds` `Filter.Eventually.exists` `nhdsGT_neBot` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `Filter.Eventually.and` `self_mem_nhdsWithin` `Set.singleton_add` `Set.image_add_left` `add_neg_cancel_left` `add_sub_cancel` `norm_add_le` `le_imp_le_of_le_of_le` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mem_closedBall_iff_norm` `le_refl` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `norm_smul` `NormedSpace.toNormSMulClass` `abs_of_nonneg` `LT.lt.le` `smul_sub` `add_sub_cancel_left` `sub_sub_sub_cancel_left` `norm_sub_le` `add_le_add` `covariant_swap_add_of_covariant_add` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `le_of_lt` `mul_pos` `Right.add_pos_of_nonneg_of_pos` `NNReal.coe_nonneg` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.const_add_termg` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Abel.zero_termg` `mul_le_mul_iff_right₀` `mul_assoc` `ContinuousLinearMap.le_opNorm` `mem_closedBall_iff_norm'` `norm_nonneg` `Filter.Tendsto.mono_left` `Continuous.tendsto` `Continuous.fun_add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Continuous.comp'` `continuous_mul` `IsTopologicalSemiring.toContinuousMul` `Continuous.prodMk` `continuous_const` `continuous_id'` `Continuous.fun_mul` `le_of_tendsto_of_tendsto` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `tendsto_const_nhds` `add_zero` `MulZeroClass.mul_zero`

MeasurableEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul` 📖	mathematical	`MeasurableSet` `MeasurableEmbedding` `Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.IntegrableOn` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Set.image` `HasFDerivWithinAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `SeminormedAddCommGroup.toPseudoMetricSpace`	`DFunLike.coe` `Set` `ENNReal` `MeasureTheory.Measure.comap` `MeasureTheory.Measure.withDensity` `ENNReal.ofReal` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `MeasureTheory.Measure.restrict` `Real.instMul` `abs` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.comap_apply` `injective` `measurableSet_image'` `MeasureTheory.withDensity_apply` `MeasureTheory.ofReal_integral_eq_lintegral_ofReal` `MeasureTheory.ae_restrict_iff'` `MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul` `Function.Injective.injOn`

MeasurableEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul` 📖	mathematical	`MeasurableSet` `Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.IntegrableOn` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Set.image` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `instEquivLike` `HasFDerivWithinAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Set` `ENNReal` `MeasureTheory.Measure.map` `symm` `MeasureTheory.Measure.withDensity` `ENNReal.ofReal` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `MeasureTheory.Measure.restrict` `Real.instMul` `abs` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing`	—	`MeasureTheory.Measure.instOuterMeasureClass` `map_symm` `MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul` `measurableEmbedding`

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addHaar_image_eq_zero_of_det_fderivWithin_eq_zero` 📖	mathematical	`HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousLinearMap.det` `Real.commRing` `Real.instZero`	`DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike` `Set.image` `instZeroENNReal`	—	`addHaar_image_eq_zero_of_det_fderivWithin_eq_zero_aux` `HasFDerivWithinAt.mono` `Set.inter_subset_left` `Set.inter_subset_right` `ENNReal.Tendsto.mul_const` `ENNReal.tendsto_coe` `Filter.tendsto_id` `LT.lt.ne` `measure_closedBall_lt_top` `FiniteDimensional.proper_real` `Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `Filter.Tendsto.mono_left` `MulZeroClass.zero_mul` `nhdsWithin_le_nhds` `le_antisymm` `ge_of_tendsto` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `nhdsGT_neBot` `NNReal.instOrderTopology` `NNReal.instDenselyOrdered` `IsStrictOrderedRing.toNoMaxOrder` `NNReal.instIsStrictOrderedRing` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `Metric.iUnion_inter_closedBall_nat` `Set.image_iUnion` `measure_iUnion_le` `Measure.instOuterMeasureClass` `instCountableNat` `tsum_zero`
`addHaar_image_eq_zero_of_det_fderivWithin_eq_zero_aux` 📖	mathematical	`HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instHasSubset` `Metric.closedBall` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `ContinuousLinearMap.det` `Real.commRing` `Real.instZero`	`ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Measure.instFunLike` `Set.image` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	—	`Set.eq_empty_or_nonempty` `Set.image_empty` `measure_empty` `Measure.instOuterMeasureClass` `ENNReal.instCanonicallyOrderedAdd` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftMono` `NNReal.addLeftReflectLT` `Filter.Eventually.exists` `nhdsGT_neBot` `NNReal.instOrderTopology` `NNReal.instDenselyOrdered` `IsStrictOrderedRing.toNoMaxOrder` `NNReal.instIsStrictOrderedRing` `Filter.Eventually.and` `addHaar_image_le_mul_of_det_lt` `self_mem_nhdsWithin` `exists_partition_approximatesLinearOn_of_hasFDerivWithinAt` `secondCountable_of_proper` `FiniteDimensional.proper_real` `LT.lt.ne'` `Set.image_iUnion` `Set.inter_iUnion` `measure_mono` `Set.image_mono` `Set.subset_inter` `Set.Subset.rfl` `measure_iUnion_le` `instCountableNat` `Summable.tsum_le_tsum` `ENNReal.instIsOrderedAddMonoid` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `SummationFilter.instNeBotUnconditional` `ENNReal.summable` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.toNNReal_zero` `zero_add` `ENNReal.tsum_mul_left` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `Set.inter_subset_inter` `subset_refl` `Set.instReflSubset` `measure_iUnion` `pairwise_disjoint_mono` `Set.inter_subset_right` `MeasurableSet.inter` `measurableSet_closedBall` `BorelSpace.opensMeasurable` `le_imp_le_of_le_of_le` `Set.inter_subset_left` `le_refl`
`addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero` 📖	mathematical	`DifferentiableOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike` `instZeroENNReal`	`Set.image`	—	`le_antisymm` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftMono` `NNReal.addLeftReflectLT` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `Filter.Eventually.exists` `nhdsGT_neBot` `NNReal.instOrderTopology` `NNReal.instDenselyOrdered` `IsStrictOrderedRing.toNoMaxOrder` `Filter.Eventually.and` `addHaar_image_le_mul_of_det_lt` `self_mem_nhdsWithin` `exists_partition_approximatesLinearOn_of_hasFDerivWithinAt` `secondCountable_of_proper` `FiniteDimensional.proper_real` `DifferentiableWithinAt.hasFDerivWithinAt` `LT.lt.ne'` `measure_mono` `Measure.instOuterMeasureClass` `Set.image_iUnion` `Set.inter_iUnion` `Set.image_mono` `Set.subset_inter` `Set.Subset.rfl` `measure_iUnion_le` `instCountableNat` `ENNReal.tsum_le_tsum` `Summable.tsum_le_tsum` `ENNReal.instIsOrderedAddMonoid` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `SummationFilter.instNeBotUnconditional` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `le_trans` `Set.inter_subset_left` `le_of_eq` `ENNReal.summable` `MulZeroClass.mul_zero` `tsum_zero` `zero_le` `ENNReal.instCanonicallyOrderedAdd`
`addHaar_image_le_lintegral_abs_det_fderiv` 📖	mathematical	`MeasurableSet` `HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Set.image` `lintegral` `Measure.restrict` `ENNReal.ofReal` `abs` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing`	—	`Measure.IsAddHaarMeasure.sigmaFinite` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `FiniteDimensional.proper_real` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `MeasurableSet.disjointed` `measurableSet_spanningSets` `Set.inter_iUnion` `iUnion_disjointed` `iUnion_spanningSets` `Set.inter_univ` `Set.image_iUnion` `measure_iUnion_le` `Measure.instOuterMeasureClass` `instCountableNat` `ENNReal.tsum_le_tsum` `addHaar_image_le_lintegral_abs_det_fderiv_aux2` `MeasurableSet.inter` `lt_of_le_of_lt` `measure_mono` `disjointed_subset` `measure_spanningSets_lt_top` `ne_of_lt` `Set.inter_subset_right` `HasFDerivWithinAt.mono` `Set.inter_subset_left` `lintegral_iUnion` `pairwise_disjoint_mono` `disjoint_disjointed`
`addHaar_image_le_lintegral_abs_det_fderiv_aux1` 📖	mathematical	`MeasurableSet` `HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Set.image` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `lintegral` `Measure.restrict` `ENNReal.ofReal` `abs` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing` `Distrib.toMul` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `ENNReal.ofNNReal`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftMono` `NNReal.addLeftReflectLT` `Filter.Eventually.exists` `nhdsGT_neBot` `NNReal.instOrderTopology` `NNReal.instDenselyOrdered` `IsStrictOrderedRing.toNoMaxOrder` `NNReal.instIsStrictOrderedRing` `Filter.Eventually.and` `addHaar_image_le_mul_of_det_lt` `self_mem_nhdsWithin` `RingHomIsometric.ids` `Metric.continuousAt_iff` `Continuous.continuousAt` `ContinuousLinearMap.continuous_det` `Real.instCompleteSpace` `Nat.instAtLeastTwoHAddOfNat` `LT.lt.le` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `lt_min` `Real.dist_eq` `dist_eq_norm` `NNReal.coe_min` `half_lt_self` `ApproximatesLinearOn.mono_num` `min_le_left` `exists_partition_approximatesLinearOn_of_hasFDerivWithinAt` `secondCountable_of_proper` `FiniteDimensional.proper_real` `LT.lt.ne'` `measure_mono` `Measure.instOuterMeasureClass` `Set.image_iUnion` `Set.inter_iUnion` `Set.image_mono` `Set.subset_inter` `Set.Subset.rfl` `measure_iUnion_le` `instCountableNat` `ENNReal.tsum_le_tsum` `lintegral_const` `Measure.restrict_apply` `Set.univ_inter` `lintegral_mono_ae` `Filter.mp_mem` `ApproximatesLinearOn.norm_fderiv_sub_le` `MeasurableSet.inter` `HasFDerivWithinAt.mono` `Set.inter_subset_left` `Filter.univ_mem'` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.isInt_add` `zero_add` `Mathlib.Tactic.Abel.zero_termg` `abs_sub` `Real.instIsOrderedAddMonoid` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `le_rfl` `add_le_add_left` `ENNReal.instIsOrderedAddMonoid` `ENNReal.ofReal_le_ofReal` `ENNReal.ofReal_add` `ENNReal.ofReal_coe_nnreal` `add_assoc` `two_mul` `lintegral_iUnion` `pairwise_disjoint_mono` `Set.inter_subset_right` `Set.inter_eq_self_of_subset_left` `lintegral_add_right'` `aemeasurable_const` `setLIntegral_const`
`addHaar_image_le_lintegral_abs_det_fderiv_aux2` 📖	mathematical	`MeasurableSet` `HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Set.image` `lintegral` `Measure.restrict` `ENNReal.ofReal` `abs` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing`	—	`Nat.instAtLeastTwoHAddOfNat` `Filter.Tendsto.mono_left` `Filter.Tendsto.add` `ENNReal.instContinuousAdd` `tendsto_const_nhds` `ENNReal.Tendsto.mul_const` `ENNReal.Tendsto.const_mul` `ENNReal.tendsto_coe` `Filter.tendsto_id` `ENNReal.coe_ne_top` `nhdsWithin_le_nhds` `ge_of_tendsto` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `nhdsGT_neBot` `NNReal.instOrderTopology` `NNReal.instDenselyOrdered` `IsStrictOrderedRing.toNoMaxOrder` `NNReal.instIsStrictOrderedRing` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `add_zero` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'` `addHaar_image_le_lintegral_abs_det_fderiv_aux1` `Set.mem_Ioi`
`addHaar_image_le_mul_of_det_lt` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofReal` `abs` `Real` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `ENNReal.ofNNReal`	`Filter.Eventually` `NNReal` `nhdsWithin` `NNReal.instTopologicalSpace` `instZeroNNReal` `Set.Ioi` `instPartialOrderNNReal`	—	`nhdsWithin_le_nhds` `IsCompact.image` `ProperSpace.isCompact_closedBall` `FiniteDimensional.proper_real` `ContinuousLinearMap.continuous` `Filter.Tendsto.mono_left` `tendsto_measure_cthickening_of_isCompact` `BorelSpace.opensMeasurable` `Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `Filter.Tendsto.congr'` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'` `IsCompact.add_closedBall_zero` `le_of_lt` `add_comm` `Measure.addHaar_image_continuousLinearMap` `ENNReal.mul_lt_mul_left` `LT.lt.ne'` `Metric.measure_closedBall_pos` `Measure.IsAddHaarMeasure.toIsOpenPosMeasure` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `LT.lt.ne` `measure_closedBall_lt_top` `tendsto_order` `ENNReal.instOrderTopology` `Filter.Eventually.exists` `nhdsGT_neBot` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `Filter.Eventually.and` `LT.lt.le` `Iio_mem_nhds` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `NNReal.instOrderTopology` `Set.mem_add` `Set.mem_image_of_mem` `dist_eq_norm` `sub_zero` `mem_closedBall_iff_norm` `add_sub_cancel_right` `mul_le_mul` `IsOrderedRing.toPosMulMono` `IsOrderedRing.toMulPosMono` `norm_nonneg` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Abel.zero_termg` `smul_add` `add_assoc` `smul_closedBall` `smul_zero` `singleton_add_closedBall_zero` `image_smul_set` `SemilinearMapClass.toMulActionSemiHomClass` `zero_le_one` `Real.norm_eq_abs` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_one` `mul_comm` `measure_mono` `Measure.instOuterMeasureClass` `Set.singleton_add` `Set.image_add_left` `measure_preimage_add` `ContinuousAdd.measurableAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Measure.IsAddHaarMeasure.toIsAddLeftInvariant` `Measure.addHaar_smul` `abs_pow` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `Measure.addHaar_closedBall'` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Besicovitch.exists_closedBall_covering_tsum_measure_le` `UniformSpace.secondCountable_of_separable` `EMetric.instIsCountablyGeneratedUniformity` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `Besicovitch.instHasBesicovitchCovering` `instSFiniteOfSigmaFinite` `Measure.IsAddHaarMeasure.sigmaFinite` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `Measure.WeaklyRegular.toOuterRegular` `Measure.WeaklyRegular.of_pseudoMetrizableSpace_secondCountable_of_locallyFinite` `PseudoEMetricSpace.pseudoMetrizableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `instLindelofSpaceOfSigmaCompactSpace` `sigmaCompactSpace_of_locallyCompact_secondCountable` `isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts` `Set.mem_Ioi` `Nat.instAtLeastTwoHAddOfNat` `half_pos` `Set.image_iUnion` `Set.inter_iUnion` `Set.image_mono` `Set.subset_inter` `Set.Subset.refl` `Set.biUnion_eq_iUnion` `measure_iUnion_le` `Encodable.countable` `ENNReal.tsum_le_tsum` `ENNReal.tsum_mul_left` `ENNReal.Tendsto.const_mul` `Filter.Tendsto.add` `ENNReal.instContinuousAdd` `tendsto_const_nhds` `Filter.tendsto_id` `ge_of_tendsto` `ENNReal.nhdsGT_zero_neBot`
`aemeasurable_fderivWithin` 📖	mathematical	`MeasurableSet` `HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`AEMeasurable` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.instMeasurableSpace` `Measure.restrict`	—	`aemeasurable_of_unif_approx` `RingHomIsometric.ids` `ContinuousLinearMap.instBorelSpace` `le_of_lt` `Measure.instOuterMeasureClass` `exists_partition_approximatesLinearOn_of_hasFDerivWithinAt` `secondCountable_of_proper` `FiniteDimensional.proper_real` `LT.lt.ne'` `exists_measurable_piecewise` `instCountableNat` `measurable_const` `Pairwise.mono` `Disjoint.inter_eq` `Measurable.aemeasurable` `Measure.ae_sum_iff` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ApproximatesLinearOn.norm_fderiv_sub_le` `MeasurableSet.inter` `HasFDerivWithinAt.mono` `Set.inter_subset_left` `Filter.mp_mem` `ae_restrict_mem` `Filter.univ_mem'` `ae_mono` `Measure.restrict_mono` `Set.inter_subset_right` `le_rfl` `dist_comm` `nndist_eq_nnnorm` `Set.inter_iUnion` `Set.Subset.antisymm` `Set.subset_inter` `Set.Subset.rfl` `Measure.restrict_iUnion_le`
`aemeasurable_ofReal_abs_det_fderivWithin` 📖	mathematical	`MeasurableSet` `HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `ENNReal.ofReal` `abs` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing` `Measure.restrict`	—	`Measurable.comp_aemeasurable` `ENNReal.measurable_ofReal` `Continuous.measurable` `BorelSpace.opensMeasurable` `Real.borelSpace` `continuous_abs` `Real.instIsOrderedAddMonoid` `instOrderTopologyReal` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.instBorelSpace` `ContinuousLinearMap.continuous_det` `Real.instCompleteSpace` `aemeasurable_fderivWithin`
`aemeasurable_toNNReal_abs_det_fderivWithin` 📖	mathematical	`MeasurableSet` `HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`AEMeasurable` `NNReal` `NNReal.measurableSpace` `Real.toNNReal` `abs` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing` `Measure.restrict`	—	`Measurable.comp_aemeasurable` `measurable_real_toNNReal` `Continuous.measurable` `BorelSpace.opensMeasurable` `Real.borelSpace` `continuous_abs` `Real.instIsOrderedAddMonoid` `instOrderTopologyReal` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.instBorelSpace` `ContinuousLinearMap.continuous_det` `Real.instCompleteSpace` `aemeasurable_fderivWithin`
`integrableOn_image_iff_integrableOn_abs_det_fderiv_smul` 📖	mathematical	`MeasurableSet` `HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.InjOn`	`IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.image` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `abs` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing`	—	`IntegrableOn.eq_1` `restrict_map_withDensity_abs_det_fderiv_eq_addHaar` `MeasurableEmbedding.integrable_map_iff` `measurableEmbedding_of_fderivWithin` `MeasurableEmbedding.subtype_coe` `map_comap_subtype_coe` `restrict_withDensity` `integrable_withDensity_iff_integrable_coe_smul₀` `aemeasurable_toNNReal_abs_det_fderivWithin` `Real.coe_toNNReal` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`integral_image_eq_integral_abs_det_fderiv_smul` 📖	mathematical	`MeasurableSet` `HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.InjOn`	`integral` `Measure.restrict` `Set.image` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `abs` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing`	—	`restrict_map_withDensity_abs_det_fderiv_eq_addHaar` `MeasurableEmbedding.integral_map` `measurableEmbedding_of_fderivWithin` `MeasurableEmbedding.subtype_coe` `map_comap_subtype_coe` `setIntegral_withDensity_eq_setIntegral_smul₀` `aemeasurable_toNNReal_abs_det_fderivWithin` `NNReal.smul_def` `Real.coe_toNNReal` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`integral_target_eq_integral_abs_det_fderiv_smul` 📖	mathematical	`HasFDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `OpenPartialHomeomorph.toFun'`	`integral` `Measure.restrict` `PartialEquiv.target` `OpenPartialHomeomorph.toPartialEquiv` `PartialEquiv.source` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `abs` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing`	—	`PartialEquiv.image_source_eq_target` `integral_image_eq_integral_abs_det_fderiv_smul` `IsOpen.measurableSet` `BorelSpace.opensMeasurable` `OpenPartialHomeomorph.open_source` `HasFDerivAt.hasFDerivWithinAt` `OpenPartialHomeomorph.injOn`
`lintegral_abs_det_fderiv_eq_addHaar_image` 📖	mathematical	`MeasurableSet` `HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.InjOn`	`lintegral` `Measure.restrict` `ENNReal.ofReal` `abs` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing` `DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike` `Set.image`	—	`le_antisymm` `lintegral_abs_det_fderiv_le_addHaar_image` `addHaar_image_le_lintegral_abs_det_fderiv`
`lintegral_abs_det_fderiv_eq_addHaar_image₀` 📖	mathematical	`NullMeasurableSet` `HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.InjOn`	`lintegral` `Measure.restrict` `ENNReal.ofReal` `abs` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing` `DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike` `Set.image`	—	`Measure.instOuterMeasureClass` `NullMeasurableSet.exists_measurable_subset_ae_eq` `measure_congr` `Set.union_diff_self` `Set.union_eq_self_of_subset_left` `Set.image_union` `union_ae_eq_left_of_ae_eq_empty` `ae_eq_empty` `addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero` `DifferentiableWithinAt.mono` `HasFDerivWithinAt.differentiableWithinAt` `Set.diff_subset` `ae_eq_set` `setLIntegral_congr` `Filter.EventuallyEq.symm` `lintegral_abs_det_fderiv_eq_addHaar_image` `HasFDerivWithinAt.mono` `Set.InjOn.mono`
`lintegral_abs_det_fderiv_le_addHaar_image` 📖	mathematical	`MeasurableSet` `HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.InjOn`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `lintegral` `Measure.restrict` `ENNReal.ofReal` `abs` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Set.image`	—	`Measure.IsAddHaarMeasure.sigmaFinite` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `FiniteDimensional.proper_real` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `MeasurableSet.disjointed` `measurableSet_spanningSets` `Set.inter_iUnion` `iUnion_disjointed` `iUnion_spanningSets` `Set.inter_univ` `lintegral_iUnion` `instCountableNat` `MeasurableSet.inter` `pairwise_disjoint_mono` `disjoint_disjointed` `Set.inter_subset_right` `ENNReal.tsum_le_tsum` `lintegral_abs_det_fderiv_le_addHaar_image_aux2` `lt_of_le_of_lt` `measure_mono` `Measure.instOuterMeasureClass` `disjointed_subset` `measure_spanningSets_lt_top` `ne_of_lt` `HasFDerivWithinAt.mono` `Set.inter_subset_left` `Set.InjOn.mono` `Set.image_iUnion` `measure_iUnion` `Disjoint.image` `Disjoint.mono` `measurable_image_of_fderivWithin`
`lintegral_abs_det_fderiv_le_addHaar_image_aux1` 📖	mathematical	`MeasurableSet` `HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.InjOn` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `lintegral` `Measure.restrict` `ENNReal.ofReal` `abs` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Set.image` `Distrib.toMul` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `ENNReal.ofNNReal`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomIsometric.ids` `Metric.continuousAt_iff` `Continuous.continuousAt` `ContinuousLinearMap.continuous_det` `Real.instCompleteSpace` `Nat.instAtLeastTwoHAddOfNat` `LT.lt.le` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.dist_eq` `dist_eq_norm` `LE.le.trans_lt` `half_lt_self` `eq_or_ne` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `ENNReal.ofReal_zero` `MulZeroClass.zero_mul` `ENNReal.instCanonicallyOrderedAdd` `AddTorsor.nonempty` `ENNReal.coe_sub` `ENNReal.sub_lt_self` `ENNReal.coe_ne_top` `covariant_swap_add_of_covariant_add` `LT.lt.ne'` `Filter.Eventually.exists` `nhdsGT_neBot` `NNReal.instOrderTopology` `NNReal.instDenselyOrdered` `IsStrictOrderedRing.toNoMaxOrder` `NNReal.instIsStrictOrderedRing` `Filter.Eventually.and` `mul_le_addHaar_image_of_lt_det` `self_mem_nhdsWithin` `lt_min` `LE.le.trans` `NNReal.coe_min` `ENNReal.mul_top` `add_top` `ApproximatesLinearOn.mono_num` `min_le_left` `tsub_le_iff_right` `ENNReal.instOrderedSub` `ENNReal.sub_mul` `exists_partition_approximatesLinearOn_of_hasFDerivWithinAt` `secondCountable_of_proper` `FiniteDimensional.proper_real` `Set.inter_iUnion` `Set.Subset.antisymm` `Set.subset_inter` `Set.Subset.rfl` `Set.inter_subset_left` `lintegral_iUnion` `instCountableNat` `MeasurableSet.inter` `pairwise_disjoint_mono` `Set.inter_subset_right` `ENNReal.tsum_le_tsum` `lintegral_mono_ae` `Filter.mp_mem` `Measure.instOuterMeasureClass` `ApproximatesLinearOn.norm_fderiv_sub_le` `HasFDerivWithinAt.mono` `Filter.univ_mem'` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Tactic.Abel.zero_termg` `abs_add_le` `add_le_add` `le_rfl` `ENNReal.ofReal_le_ofReal` `ENNReal.ofReal_add` `ENNReal.ofReal_coe_nnreal` `lintegral_add_right` `measurable_const` `setLIntegral_const` `Summable.tsum_le_tsum` `ENNReal.instIsOrderedAddMonoid` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `SummationFilter.instNeBotUnconditional` `add_le_add_left` `ENNReal.summable` `Set.image_iUnion` `measure_iUnion` `Disjoint.image` `Disjoint.mono` `measurable_image_of_fderivWithin` `Set.InjOn.mono` `ENNReal.tsum_mul_left` `ENNReal.tsum_add` `mul_assoc` `two_mul` `add_assoc`
`lintegral_abs_det_fderiv_le_addHaar_image_aux2` 📖	mathematical	`MeasurableSet` `HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.InjOn`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `lintegral` `Measure.restrict` `ENNReal.ofReal` `abs` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Set.image`	—	`Nat.instAtLeastTwoHAddOfNat` `Filter.Tendsto.mono_left` `Filter.Tendsto.add` `ENNReal.instContinuousAdd` `tendsto_const_nhds` `ENNReal.Tendsto.mul_const` `ENNReal.Tendsto.const_mul` `ENNReal.tendsto_coe` `Filter.tendsto_id` `ENNReal.coe_ne_top` `nhdsWithin_le_nhds` `ge_of_tendsto` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `nhdsGT_neBot` `NNReal.instOrderTopology` `NNReal.instDenselyOrdered` `IsStrictOrderedRing.toNoMaxOrder` `NNReal.instIsStrictOrderedRing` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `add_zero` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'` `lintegral_abs_det_fderiv_le_addHaar_image_aux1` `Set.mem_Ioi`
`lintegral_image_eq_lintegral_abs_det_fderiv_mul` 📖	mathematical	`MeasurableSet` `HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.InjOn`	`lintegral` `Measure.restrict` `Set.image` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofReal` `abs` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing`	—	`restrict_map_withDensity_abs_det_fderiv_eq_addHaar` `MeasurableEmbedding.lintegral_map` `measurableEmbedding_of_fderivWithin` `MeasurableEmbedding.subtype_coe` `map_comap_subtype_coe` `setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀` `aemeasurable_ofReal_abs_det_fderivWithin` `Measure.instOuterMeasureClass`
`map_withDensity_abs_det_fderiv_eq_addHaar` 📖	mathematical	`NullMeasurableSet` `HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.InjOn`	`Measure.map` `Measure.withDensity` `Measure.restrict` `ENNReal.ofReal` `abs` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing` `Set.image`	—	`ContinuousOn.aemeasurable₀` `BorelSpace.opensMeasurable` `DifferentiableWithinAt.continuousWithinAt` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `HasFDerivWithinAt.differentiableWithinAt` `AEMeasurable.mono_ac` `withDensity_absolutelyContinuous` `Measure.ext` `AEMeasurable.nullMeasurableSet_preimage` `Measure.map_apply_of_aemeasurable` `withDensity_apply₀` `Measure.restrict_apply` `Measure.restrict_restrict₀` `lintegral_abs_det_fderiv_eq_addHaar_image₀` `nullMeasurableSet_restrict` `HasFDerivWithinAt.mono` `Set.inter_subset_right` `Set.InjOn.mono` `Set.image_preimage_inter`
`measurableEmbedding_of_fderivWithin` 📖	mathematical	`MeasurableSet` `HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.InjOn`	`MeasurableEmbedding` `Set.Elem` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `Set.restrict`	—	`ContinuousOn.measurableEmbedding` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `FiniteDimensional.proper_real` `TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable` `complete_of_proper` `EMetric.instIsCountablyGeneratedUniformity` `T6Space.toT0Space` `instT6SpaceOfMetrizableSpace` `DifferentiableOn.continuousOn` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `HasFDerivWithinAt.differentiableWithinAt`
`measurable_image_of_fderivWithin` 📖	mathematical	`MeasurableSet` `HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.InjOn`	`Set.image`	—	`MeasurableSet.image_of_continuousOn_injOn` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `BorelSpace.opensMeasurable` `instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `FiniteDimensional.proper_real` `TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable` `complete_of_proper` `EMetric.instIsCountablyGeneratedUniformity` `T6Space.toT0Space` `instT6SpaceOfMetrizableSpace` `DifferentiableOn.continuousOn` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `HasFDerivWithinAt.differentiableWithinAt`
`mul_le_addHaar_image_of_lt_det` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `ENNReal.ofReal` `abs` `Real` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField`	`Filter.Eventually` `NNReal` `nhdsWithin` `NNReal.instTopologicalSpace` `instZeroNNReal` `Set.Ioi` `instPartialOrderNNReal`	—	`nhdsWithin_le_nhds` `eq_or_lt_of_le` `zero_le` `NNReal.instCanonicallyOrderedAdd` `Filter.univ_mem'` `MulZeroClass.zero_mul` `ENNReal.instCanonicallyOrderedAdd` `AddTorsor.nonempty` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `ENNReal.ofReal_zero` `RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Real.instCompleteSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `ContinuousLinearEquiv.det_coe_symm` `abs_inv` `Real.instIsStrictOrderedRing` `Real.toNNReal_inv` `NNReal.inv_lt_inv` `LT.lt.ne'` `addHaar_image_le_mul_of_det_lt` `Filter.Eventually.exists` `nhdsGT_neBot` `NNReal.instOrderTopology` `NNReal.instDenselyOrdered` `IsStrictOrderedRing.toNoMaxOrder` `NNReal.instIsStrictOrderedRing` `Filter.Eventually.and` `self_mem_nhdsWithin` `RingHomIsometric.ids` `nhds_neBot` `Iio_mem_nhds` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_pos` `eq_or_ne` `tendsto_const_nhds` `Filter.Tendsto.mul` `IsTopologicalSemiring.toContinuousMul` `NNReal.instIsTopologicalSemiring` `Filter.Tendsto.inv₀` `NNReal.instContinuousInv₀` `Filter.Tendsto.sub` `NNReal.instContinuousSub` `Filter.tendsto_id` `tsub_zero` `NNReal.instOrderedSub` `tendsto_order` `MulZeroClass.mul_zero` `Filter.mp_mem` `ApproximatesLinearOn.mono_num` `LT.lt.le` `ApproximatesLinearOn.to_inv` `PartialEquiv.symm_image_target_eq_source` `mul_comm` `ENNReal.le_div_iff_mul_le` `div_eq_mul_inv` `ENNReal.coe_inv`
`nullMeasurable_image_of_fderivWithin` 📖	mathematical	`NullMeasurableSet` `HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.InjOn`	`Set.image`	—	`Measure.instOuterMeasureClass` `NullMeasurableSet.exists_measurable_subset_ae_eq` `Set.union_diff_self` `Set.union_eq_self_of_subset_left` `Set.image_union` `union_ae_eq_left_of_ae_eq_empty` `ae_eq_empty` `addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero` `DifferentiableWithinAt.mono` `HasFDerivWithinAt.differentiableWithinAt` `Set.diff_subset` `ae_eq_set` `NullMeasurableSet.congr` `MeasurableSet.nullMeasurableSet` `measurable_image_of_fderivWithin` `HasFDerivWithinAt.mono` `Set.InjOn.mono` `Filter.EventuallyEq.symm`
`restrict_map_withDensity_abs_det_fderiv_eq_addHaar` 📖	mathematical	`MeasurableSet` `HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.InjOn`	`Measure.map` `Set.Elem` `Subtype.instMeasurableSpace` `Set` `Set.instMembership` `Set.restrict` `Measure.comap` `Measure.withDensity` `ENNReal.ofReal` `abs` `Real.lattice` `Real.instAddGroup` `ContinuousLinearMap.det` `Real.commRing` `Measure.restrict` `Set.image`	—	`ContinuousOn.measurable_piecewise` `BorelSpace.opensMeasurable` `HasFDerivWithinAt.differentiableWithinAt` `DifferentiableOn.continuousOn` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Continuous.continuousOn` `continuous_zero` `Set.piecewise_eqOn` `HasFDerivWithinAt.congr` `Measure.map_map` `measurable_subtype_coe` `map_comap_subtype_coe` `restrict_withDensity` `map_withDensity_abs_det_fderiv_eq_addHaar` `MeasurableSet.nullMeasurableSet` `Set.InjOn.congr` `Set.EqOn.symm` `Set.EqOn.image_eq`

WeierstrassCurve

Definitions

Name	Category	Theorems
`Jacobian` 📖	CompOp	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt` 📖	mathematical	`HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`IsClosed` `Set` `Set.instHasSubset` `Set.iUnion` `ApproximatesLinearOn` `Set.instInter` `Set.instMembership`	—	`Set.eq_empty_or_nonempty` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `Set.iUnion_empty` `Set.instReflSubset` `Set.inter_self` `AddTorsor.nonempty` `RingHomIsometric.ids` `TopologicalSpace.isOpen_iUnion_countable` `instSecondCountableTopologyContinuousLinearMapIdOfFiniteDimensional` `Real.instCompleteSpace` `Metric.isOpen_ball` `exists_seq_strictAnti_tendsto` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `Set.mem_iUnion` `dist_self` `Ne.bot_lt` `bex_def` `Set.mem_iUnion₂` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mem_ball_iff_norm` `le_of_eq` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isInt_neg` `zero_add` `Mathlib.Tactic.Abel.zero_termg` `Metric.mem_nhdsWithin_iff` `Asymptotics.IsLittleO.def` `HasFDerivAtFilter.isLittleO` `Filter.Eventually.exists` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `tendsto_order` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `Mathlib.Tactic.Abel.term_add_constg` `norm_add_le` `add_le_add` `Set.inter_comm` `Set.inter_subset_inter_right` `Metric.ball_subset_ball` `LT.lt.le` `ContinuousLinearMap.le_opNorm` `add_mul` `Distrib.rightDistribClass` `add_comm` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `norm_nonneg` `mem_closure_iff_seq_limit` `FirstCountableTopology.frechetUrysohnSpace` `Filter.Tendsto.norm` `Filter.Tendsto.comp` `ContinuousWithinAt.tendsto` `HasFDerivWithinAt.continuousWithinAt` `IsTopologicalAddGroup.toContinuousAdd` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within` `Filter.Eventually.of_forall` `Filter.Tendsto.sub` `IsTopologicalAddGroup.to_continuousSub` `tendsto_const_nhds` `Continuous.tendsto` `ContinuousLinearMap.continuous` `Filter.Tendsto.const_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Filter.Tendsto.dist` `Filter.mp_mem` `Filter.univ_mem'` `le_of_tendsto_of_tendsto` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `TopologicalSpace.exists_dense_seq` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `FiniteDimensional.proper_real` `Nat.instAtLeastTwoHAddOfNat` `dist_triangle_right` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Nat.cast_one` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `CancelDenoms.sub_subst` `CancelDenoms.add_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Meta.NormNum.isNat_lt_true` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `IsClosed.inter` `isClosed_closure` `Metric.isClosed_closedBall` `Encodable.surjective_decode_getD` `DenseRange.exists_mem_open` `Metric.mem_ball'` `subset_closure`
`exists_partition_approximatesLinearOn_of_hasFDerivWithinAt` 📖	mathematical	`HasFDerivWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Pairwise` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `MeasurableSet` `Set.instHasSubset` `Set.iUnion` `ApproximatesLinearOn` `Set.instInter` `Set.instMembership`	—	`exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt` `disjoint_disjointed` `MeasurableSet.disjointed` `IsClosed.measurableSet` `BorelSpace.opensMeasurable` `iUnion_disjointed` `ApproximatesLinearOn.mono_set` `Set.inter_subset_inter_right` `disjointed_subset`

---

← Back to Index