FiniteDimension

📁 Source: Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

Statistics

Metric	Count
Definitions `u`, `w`, `y`, `φ`	4
Theorems `instHasContDiffBumpOfFiniteDimensionalReal`, `u_compact_support`, `u_continuous`, `u_exists`, `u_int_pos`, `u_le_one`, `u_neg`, `u_nonneg`, `u_smooth`, `u_support`, `w_compact_support`, `w_def`, `w_integral`, `w_mul_φ_nonneg`, `w_nonneg`, `w_support`, `y_eq_one_of_mem_closedBall`, `y_eq_zero_of_notMem_ball`, `y_le_one`, `y_neg`, `y_nonneg`, `y_pos_of_mem_ball`, `y_smooth`, `y_support`, `exists_contDiff_support_eq`, `exists_smooth_support_eq`, `exists_contDiff_tsupport_subset`, `exists_smooth_tsupport_subset`	28
Total	32

ExistsContDiffBumpBase

Definitions

Name	Category	Theorems
`u` 📖	CompOp	9 math math: `u_support`, `u_continuous`, `u_le_one`, `u_neg`, `u_int_pos`, `u_smooth`, `w_def`, `u_compact_support`, `u_nonneg`
`w` 📖	CompOp	6 math math: `w_compact_support`, `w_support`, `w_def`, `w_integral`, `w_nonneg`, `w_mul_φ_nonneg`
`y` 📖	CompOp	8 math math: `y_eq_one_of_mem_closedBall`, `y_eq_zero_of_notMem_ball`, `y_pos_of_mem_ball`, `y_nonneg`, `y_smooth`, `y_neg`, `y_support`, `y_le_one`
`φ` 📖	CompOp	1 math math: `w_mul_φ_nonneg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasContDiffBumpOfFiniteDimensionalReal` 📖	mathematical	—	`HasContDiffBump`	—	`div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.atom_pf` `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.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.mul_neg` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.isNat_lt_true` `RCLike.charZero_rclike` `y_nonneg` `y_le_one` `Real.instZeroLEOneClass` `y.congr_simp` `smul_neg` `y_neg` `ContDiffOn.comp` `y_smooth` `ContDiffOn.prodMk` `ContDiffOn.div` `ContDiffOn.sub` `contDiffOn_fst` `contDiffOn_const` `ContDiffOn.add` `ne_of_gt` `ContDiffOn.smul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left` `ContDiffOn.inv` `ContDiffOn.div_const` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `CancelDenoms.add_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` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_nonpos` `contDiffOn_snd` `div_lt_one` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `ContDiffOn.congr` `y_eq_one_of_mem_closedBall` `inv_div` `norm_smul` `NormedSpace.toNormSMulClass` `abs_div` `abs_two` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `LT.lt.le` `mul_le_of_le_one_right` `IsOrderedRing.toPosMulMono` `le_of_lt` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `add_pos'` `lt_trans` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `support_comp_inv_smul₀` `LT.lt.ne'` `y_support` `smul_ball` `smul_zero` `Real.norm_of_nonneg` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Meta.NormNum.isNat_eq_false` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.mul_pf_left`
`u_compact_support` 📖	mathematical	—	`HasCompactSupport` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.instZero` `u`	—	`hasCompactSupport_def` `u_support` `closure_ball` `one_ne_zero` `NeZero.charZero_one` `RCLike.charZero_rclike` `ProperSpace.isCompact_closedBall` `FiniteDimensional.proper_real`
`u_continuous` 📖	mathematical	—	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.pseudoMetricSpace` `u`	—	`ContDiff.continuous` `u_smooth`
`u_exists` 📖	mathematical	—	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat` `Top.top` `instTopENat` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder` `Real.instZero` `Real.instOne` `Function.support` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NegZeroClass.toNeg`	—	`Metric.isOpen_ball` `IsOpen.exists_contDiff_support_eq` `Set.mem_range_self` `Nat.instAtLeastTwoHAddOfNat` `ContDiff.div_const` `ContDiff.add` `ContDiff.comp` `contDiff_neg` `le_of_not_gt` `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.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `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` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_zero` `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.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `CancelDenoms.add_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_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_lt_true` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Function.support_eq_iff` `ne_of_gt` `lt_of_le_of_ne` `lt_of_not_ge` `Mathlib.Tactic.Linarith.mul_nonpos` `dist_zero_right` `norm_neg` `add_zero` `zero_div` `neg_neg` `add_comm`
`u_int_pos` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.Measure.addHaar` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `u`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `MeasureTheory.integral_pos_iff_support_of_nonneg` `u_nonneg` `Continuous.integrable_of_hasCompactSupport` `BorelSpace.opensMeasurable` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `MeasureTheory.Measure.isAddHaarMeasure_addHaarMeasure` `u_continuous` `u_compact_support` `u_support` `Metric.measure_ball_pos` `MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`u_le_one` 📖	mathematical	—	`Real` `Real.instLE` `u` `Real.instOne`	—	`u_exists`
`u_neg` 📖	mathematical	—	`u` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`u_exists`
`u_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `u`	—	`u_exists`
`u_smooth` 📖	mathematical	—	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat` `Top.top` `instTopENat` `u`	—	`u_exists`
`u_support` 📖	mathematical	—	`Function.support` `Real` `Real.instZero` `u` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instOne`	—	`u_exists`
`w_compact_support` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`HasCompactSupport` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `w`	—	`hasCompactSupport_def` `w_support` `closure_ball` `LT.lt.ne'` `ProperSpace.isCompact_closedBall` `FiniteDimensional.proper_real`
`w_def` 📖	mathematical	—	`w` `Real` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Real.instInv` `Real.instMul` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.Measure.addHaar` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `u` `Monoid.toNatPow` `Real.instMonoid` `abs` `Real.lattice` `Real.instAddGroup` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Module.toDistribMulAction`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `locallyCompact_of_proper` `FiniteDimensional.proper_real`
`w_integral` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.Measure.addHaar` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `w` `Real.instOne`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `MeasureTheory.integral_smul` `NormedSpace.toNormSMulClass` `Algebra.to_smulCommClass` `MeasureTheory.Measure.integral_comp_inv_smul_of_nonneg` `MeasureTheory.Measure.isAddHaarMeasure_addHaarMeasure` `LT.lt.le` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_comm` `mul_inv_rev` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `one_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `LT.lt.ne'` `u_int_pos` `ne_of_gt` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial`
`w_mul_φ_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `Real.instMul` `w` `φ` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `w_nonneg` `Set.indicator_nonneg` `Real.instZeroLEOneClass`
`w_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `w`	—	`mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `inv_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `LT.lt.le` `u_int_pos` `Nat.cast_zero` `pow_nonneg` `Real.instZeroLEOneClass` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `u_nonneg`
`w_support` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Function.support` `w` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`smul_unitBall` `LT.lt.ne'` `Real.norm_of_nonneg` `LT.lt.le` `Nat.cast_zero` `pow_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `w_def` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Function.support_mul` `Function.support_inv` `Function.support_const` `u_int_pos` `Set.univ_inter` `support_comp_inv_smul₀` `u_support`
`y_eq_one_of_mem_closedBall` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Set` `Set.instMembership` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instSub` `Real.instOne`	`y`	—	`Metric.ball_subset_ball'` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `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.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `NeZero.charZero_one` `RCLike.charZero_rclike` `Mathlib.Tactic.Linarith.add_neg` `Metric.mem_ball` `Metric.mem_ball_self` `Real.isBoundedSMul` `IsScalarTower.right` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `MeasureTheory.convolution_eq_right'` `le_of_eq` `w_support` `MeasureTheory.integral_mul_const` `w_integral` `one_mul`
`y_eq_zero_of_notMem_ball` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Set` `Set.instMembership` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instAdd` `Real.instOne`	`y`	—	`NeZero.charZero_one` `RCLike.charZero_rclike` `Metric.ball_subset_ball'` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `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.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `dist_zero_right` `Metric.mem_ball_comm` `Metric.mem_ball_self` `Real.isBoundedSMul` `IsScalarTower.right` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `MeasureTheory.convolution_eq_right'` `le_of_eq` `w_support` `MulZeroClass.mul_zero` `MeasureTheory.integral_const` `Real.instCompleteSpace`
`y_le_one` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real.instLE` `y` `Real.instOne`	—	`Real.isBoundedSMul` `IsScalarTower.right` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `MeasureTheory.convolution_mono_right_of_nonneg` `MeasureTheory.ConvolutionExistsAt.integrable` `HasCompactSupport.convolutionExists_left` `MeasureTheory.Measure.isAddLeftInvariant_addHaarMeasure` `MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant_of_innerRegular` `MeasureTheory.Measure.isAddHaarMeasure_addHaarMeasure` `MeasureTheory.Measure.instInnerRegularOfPseudoMetrizableSpaceOfSigmaCompactSpaceOfBorelSpaceOfSigmaFinite` `PseudoEMetricSpace.pseudoMetrizableSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `MeasureTheory.Measure.sigmaFinite_addHaarMeasure` `w_compact_support` `Continuous.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuous_const` `Continuous.comp` `u_continuous` `Continuous.const_smul` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `continuous_id'` `MeasureTheory.locallyIntegrable_const` `MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `w_nonneg` `Set.indicator_le_self'` `zero_le_one` `Real.instZeroLEOneClass` `mul_one` `w_integral` `LE.le.trans` `le_of_eq`
`y_neg` 📖	mathematical	—	`y` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`MeasureTheory.convolution_neg_of_neg_eq` `Real.isBoundedSMul` `MeasureTheory.Measure.isAddLeftInvariant_addHaarMeasure` `MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant_of_innerRegular` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.Measure.isAddHaarMeasure_addHaarMeasure` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `MeasureTheory.Measure.instInnerRegularOfPseudoMetrizableSpaceOfSigmaCompactSpaceOfBorelSpaceOfSigmaFinite` `PseudoEMetricSpace.pseudoMetrizableSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `MeasureTheory.Measure.sigmaFinite_addHaarMeasure` `ContinuousNeg.measurableNeg` `IsTopologicalAddGroup.toContinuousNeg` `ContinuousAdd.measurableAdd` `IsTopologicalAddGroup.toContinuousAdd` `Filter.univ_mem'` `MeasureTheory.Measure.instOuterMeasureClass` `w_def` `mul_inv_rev` `u.congr_simp` `smul_neg` `u_neg` `dist_zero_right` `norm_neg`
`y_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `y`	—	`MeasureTheory.integral_nonneg` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.isBoundedSMul` `w_mul_φ_nonneg`
`y_pos_of_mem_ball` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instOne` `Set` `Set.instMembership` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instAdd`	`y`	—	`MeasureTheory.integral_pos_iff_support_of_nonneg` `w_mul_φ_nonneg` `w_compact_support` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `MeasureTheory.LocallyIntegrable.indicator` `MeasureTheory.locallyIntegrable_const` `MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `MeasureTheory.Measure.isAddHaarMeasure_addHaarMeasure` `measurableSet_closedBall` `BorelSpace.opensMeasurable` `Continuous.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuous_const` `Continuous.comp` `u_continuous` `Continuous.const_smul` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `continuous_id'` `MeasureTheory.ConvolutionExistsAt.integrable` `Real.isBoundedSMul` `IsScalarTower.right` `HasCompactSupport.convolutionExists_left` `MeasureTheory.Measure.isAddLeftInvariant_addHaarMeasure` `MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant_of_innerRegular` `MeasureTheory.Measure.instInnerRegularOfPseudoMetrizableSpaceOfSigmaCompactSpaceOfBorelSpaceOfSigmaFinite` `PseudoEMetricSpace.pseudoMetrizableSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `MeasureTheory.Measure.sigmaFinite_addHaarMeasure` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `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.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_lt_true` `RCLike.charZero_rclike` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Function.support_mul` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `w_support` `NeZero.charZero_one` `Metric.ball_subset_ball'` `dist_zero_right` `norm_smul` `NormedSpace.toNormSMulClass` `abs_div` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `LT.lt.le` `Mathlib.Tactic.FieldSimp.le_eq_cancel_le` `PosMulStrictMono.toPosMulMono` `IsStrictOrderedRing.toPosMulStrictMono` `PosMulStrictMono.toPosMulReflectLE` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `LT.lt.ne'` `Mathlib.Tactic.FieldSimp.NF.cons_pos` `PosMulReflectLE.toPosMulReflectLT` `Real.instZeroLEOneClass` `zero_lt_one` `NeZero.one` `GroupWithZero.toNontrivial` `le_of_not_gt` `Real.norm_of_nonpos` `ne_of_gt` `add_pos'` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `mul_neg` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `mem_closedBall_iff_norm'` `Metric.closedBall_subset_closedBall'` `one_smul` `dist_eq_norm` `sub_smul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.mul_one` `mul_pos_of_neg_of_neg` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toMulPosStrictMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Metric.ball_subset_closedBall` `lt_of_lt_of_le` `Metric.measure_ball_pos` `MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure` `div_pos` `mul_pos` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass`
`y_smooth` 📖	mathematical	—	`ContDiffOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Prod.normedAddCommGroup` `Real.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat` `Top.top` `instTopENat` `y` `SProd.sprod` `Set` `Set.instSProd` `Set.Ioo` `Real.instPreorder` `Real.instZero` `Real.instOne` `Set.univ`	—	`isOpen_Ioo` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `ProperSpace.isCompact_closedBall` `FiniteDimensional.proper_real` `MeasureTheory.contDiffOn_convolution_left_with_param` `MeasureTheory.Measure.isAddLeftInvariant_addHaarMeasure` `MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant_of_innerRegular` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.Measure.isAddHaarMeasure_addHaarMeasure` `locallyCompact_of_proper` `MeasureTheory.Measure.instInnerRegularOfPseudoMetrizableSpaceOfSigmaCompactSpaceOfBorelSpaceOfSigmaFinite` `PseudoEMetricSpace.pseudoMetrizableSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `MeasureTheory.Measure.sigmaFinite_addHaarMeasure` `Real.isBoundedSMul` `mul_inv_rev` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Mathlib.Tactic.Contrapose.contrapose₂` `Function.mem_support` `mem_closedBall_zero_iff` `LE.le.trans` `LT.lt.le` `u_support` `norm_smul` `NormedSpace.toNormSMulClass` `abs_inv` `Real.instIsStrictOrderedRing` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `div_lt_one` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `MeasureTheory.LocallyIntegrable.indicator` `MeasureTheory.locallyIntegrable_const` `MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `measurableSet_closedBall` `BorelSpace.opensMeasurable` `ContDiffOn.mul` `Nat.cast_zero` `Nat.cast_one` `ContDiffOn.inv` `contDiffOn_const` `ContDiffOn.pow` `ContDiffOn.norm` `contDiffOn_fst` `ne_of_gt` `mul_pos` `u_int_pos` `pow_pos` `Real.instZeroLEOneClass` `abs_pos_of_pos` `ContDiff.comp_contDiffOn` `u_smooth` `ContDiffOn.smul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left` `contDiffOn_snd`
`y_support` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instOne`	`Function.support` `y` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instAdd`	—	`Function.support_eq_iff` `LT.lt.ne'` `y_pos_of_mem_ball` `y_eq_zero_of_notMem_ball`

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_contDiff_support_eq` 📖	mathematical	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Function.support` `Real` `Real.instZero` `ContDiff` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat` `Set` `Set.instHasSubset` `Set.range` `Set.Icc` `Real.instPreorder` `Real.instOne`	—	`Set.eq_empty_or_nonempty` `Function.support_zero` `contDiff_const` `Set.range_const` `AddTorsor.nonempty` `Real.instZeroLEOneClass` `Set.Subset.antisymm` `Set.iUnion_subset` `exists_contDiff_tsupport_subset` `mem_nhds` `HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_tsupport` `NeZero.charZero_one` `RCLike.charZero_rclike` `Set.mem_iUnion_of_mem` `TopologicalSpace.isOpen_iUnion_countable` `secondCountable_of_proper` `FiniteDimensional.proper_real` `Continuous.isOpen_support` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `ContDiff.continuous` `Set.Countable.exists_eq_range` `Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Set.mem_range_self` `NNReal.exists_pos_sum_of_countable` `one_ne_zero` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `instCountableNat` `Continuous.bddAbove_range_of_hasCompactSupport` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Continuous.norm` `ContDiff.continuous_iteratedFDeriv` `le_top` `HasCompactSupport.comp_left` `HasCompactSupport.iteratedFDeriv` `norm_zero` `le_trans` `Finset.le_max'` `Finset.mem_image_of_mem` `le_max_left` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `lt_max_of_lt_right` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.Positivity.nnreal_coe_pos` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `iteratedFDeriv_const_smul_apply` `ContDiffAt.of_le` `ContDiff.contDiffAt` `norm_smul` `NormedSpace.toNormSMulClass` `Real.norm_of_nonneg` `le_of_lt` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `LE.le.trans` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Summable.of_nnnorm_bounded` `Real.instCompleteSpace` `HasSum.summable` `NNReal.coe_le_coe` `coe_nnnorm` `norm_iteratedFDeriv_zero` `zero_le` `Nat.instCanonicallyOrderedAdd` `Mathlib.Tactic.Contrapose.contrapose₂` `MulZeroClass.mul_zero` `tsum_zero` `lt_of_le_of_ne` `Summable.tsum_pos` `instIsTopologicalAddGroupReal` `SummationFilter.instLeAtTopUnconditional` `SummationFilter.instNeBotUnconditional` `mul_nonneg` `LT.lt.le` `ContDiff.of_le` `contDiff_tsum_of_eventually` `instIsRCLikeNormedField` `ContDiff.const_smul` `NNReal.hasSum_coe` `Nat.cofinite_eq_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `tsum_nonneg` `HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `Summable.tsum_le_tsum` `le_abs_self`
`exists_smooth_support_eq` 📖	mathematical	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Function.support` `Real` `Real.instZero` `ContDiff` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat` `Set` `Set.instHasSubset` `Set.range` `Set.Icc` `Real.instPreorder` `Real.instOne`	—	`exists_contDiff_support_eq`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_contDiff_tsupport_subset` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Set.instHasSubset` `tsupport` `Real` `Real.instZero` `HasCompactSupport` `ContDiff` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat` `Set.range` `Set.Icc` `Real.instPreorder` `Real.instOne`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Filter.HasBasis.mem_iff` `Euclidean.nhds_basis_closedBall` `RingHomInvPair.ids` `fact_one_le_two_ennreal` `Nat.instAtLeastTwoHAddOfNat` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `half_lt_self` `hasContDiffBump_of_innerProductSpace` `ContDiffBump.support_eq` `tsupport.eq_1` `Euclidean.closure_ball` `LT.lt.ne'` `closure_mono` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Metric.isCompact_of_isClosed_isBounded` `FiniteDimensional.proper_real` `isClosed_closure` `IsCompact.isBounded` `Euclidean.isCompact_closedBall` `Bornology.IsBounded.subset` `IsClosed.closure_subset_iff` `Euclidean.isClosed_closedBall` `Euclidean.ball_subset_closedBall` `ContDiff.comp` `ContDiffBump.contDiff` `ContinuousLinearEquiv.contDiff` `ContDiffBump.nonneg` `ContDiffBump.le_one` `ContDiffBump.one_of_mem_closedBall` `Metric.mem_closedBall_self` `LT.lt.le`
`exists_smooth_tsupport_subset` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Set.instHasSubset` `tsupport` `Real` `Real.instZero` `HasCompactSupport` `ContDiff` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat` `Set.range` `Set.Icc` `Real.instPreorder` `Real.instOne`	—	`exists_contDiff_tsupport_subset`

---

← Back to Index