Documentation Verification Report

Support

📁 Source: Mathlib/Analysis/Distribution/Support.lean

Statistics

Metric	Count
Definitions `IsVanishingOn`, `dsupport`	2
Theorems `disjoint_dsupport`, `iteratedLineDerivOp`, `lineDerivOp`, `mono`, `smulLeftCLM`, `compl_dsupport_eq_sUnion_isBounded`, `dsupport_compl_eq`, `dsupport_delta`, `dsupport_iteratedLineDerivOp_subset`, `dsupport_lineDerivOp_subset`, `dsupport_smulLeftCLM_subset`, `dsupport_subset_dsupport`, `isClosed_dsupport`, `mem_dsupport_iff`, `mem_dsupport_iff_forall_exists_ne`, `mem_dsupport_iff_frequently`, `mem_dsupport_iff_not_isVanishingOn`, `notMem_dsupport_iff`, `notMem_dsupport_iff_eventually`, `not_isVanishingOn_iff`, `not_isVanishingOn_mono`, `mem_dsupport`, `notMem_dsupport`, `isVanishingOn_delta`	24
Total	26

Distribution

Definitions

Name	Category	Theorems
`IsVanishingOn` 📖	MathDef	15 math math: `mem_dsupport_iff_not_isVanishingOn`, `Filter.HasBasis.notMem_dsupport`, `IsVanishingOn.smulLeftCLM`, `not_isVanishingOn_mono`, `mem_dsupport_iff_frequently`, `notMem_dsupport_iff_eventually`, `not_isVanishingOn_iff`, `IsVanishingOn.mono`, `Filter.HasBasis.mem_dsupport`, `IsVanishingOn.iteratedLineDerivOp`, `notMem_dsupport_iff`, `compl_dsupport_eq_sUnion_isBounded`, `dsupport_compl_eq`, `TemperedDistribution.isVanishingOn_delta`, `IsVanishingOn.lineDerivOp`
`dsupport` 📖	CompOp	17 math math: `mem_dsupport_iff_not_isVanishingOn`, `dsupport_delta`, `Filter.HasBasis.notMem_dsupport`, `mem_dsupport_iff_frequently`, `notMem_dsupport_iff_eventually`, `Filter.HasBasis.mem_dsupport`, `notMem_dsupport_iff`, `dsupport_smulLeftCLM_subset`, `dsupport_iteratedLineDerivOp_subset`, `compl_dsupport_eq_sUnion_isBounded`, `dsupport_compl_eq`, `IsVanishingOn.disjoint_dsupport`, `dsupport_lineDerivOp_subset`, `isClosed_dsupport`, `dsupport_subset_dsupport`, `mem_dsupport_iff_forall_exists_ne`, `mem_dsupport_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl_dsupport_eq_sUnion_isBounded` 📖	mathematical	—	`Compl.compl` `Set` `Set.instCompl` `dsupport` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Set.sUnion` `setOf` `IsVanishingOn` `IsOpen` `Bornology.IsBounded` `PseudoMetricSpace.toBornology`	—	`Set.ext`
`dsupport_compl_eq` 📖	mathematical	—	`Compl.compl` `Set` `Set.instCompl` `dsupport` `Set.sUnion` `setOf` `IsVanishingOn` `IsOpen`	—	`Set.compl_sInter` `Set.compl_image_set_of` `compl_compl`
`dsupport_delta` 📖	mathematical	—	`dsupport` `Complex` `SchwartzMap` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `SchwartzMap.instFunLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.instZero` `DFunLike.coe` `TemperedDistribution` `Complex.instRCLike` `RCLike.innerProductSpace` `UniformConvergenceCLM.instFunLike` `Complex.instNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `SchwartzMap.instAddCommGroup` `SchwartzMap.instModule` `SchwartzMap.instTopologicalSpace` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `setOf` `Set` `Finite` `Set.Elem` `TemperedDistribution.delta` `Set.instSingletonSet`	—	`subset_antisymm` `Set.instAntisymmSubset` `mem_dsupport_iff` `TemperedDistribution.isVanishingOn_delta` `T1Space.t1` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `mem_dsupport_iff_forall_exists_ne` `exists_contDiff_tsupport_subset` `IsOpen.mem_nhds_iff` `HasSubset.Subset.trans` `Set.instIsTransSubset` `tsupport_comp_subset` `HasCompactSupport.comp_left` `ContDiff.comp` `ContinuousLinearMap.contDiff` `NeZero.charZero_one` `Complex.instCharZero`
`dsupport_iteratedLineDerivOp_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `dsupport` `Complex` `SchwartzMap` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `SchwartzMap.instFunLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `DFunLike.coe` `TemperedDistribution` `UniformConvergenceCLM.instFunLike` `Complex.instNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `SchwartzMap.instAddCommGroup` `SchwartzMap.instModule` `Complex.instRCLike` `RCLike.innerProductSpace` `SchwartzMap.instTopologicalSpace` `NormedSpace.toModule` `setOf` `Finite` `Set.Elem` `LineDeriv.iteratedLineDerivOp` `TemperedDistribution.instLineDeriv`	—	`dsupport_subset_dsupport`
`dsupport_lineDerivOp_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `dsupport` `Complex` `SchwartzMap` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `SchwartzMap.instFunLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `DFunLike.coe` `TemperedDistribution` `UniformConvergenceCLM.instFunLike` `Complex.instNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `SchwartzMap.instAddCommGroup` `SchwartzMap.instModule` `Complex.instRCLike` `RCLike.innerProductSpace` `SchwartzMap.instTopologicalSpace` `NormedSpace.toModule` `setOf` `Finite` `Set.Elem` `LineDeriv.lineDerivOp` `TemperedDistribution.instLineDeriv`	—	`dsupport_subset_dsupport`
`dsupport_smulLeftCLM_subset` 📖	mathematical	`Function.HasTemperateGrowth` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex`	`Set` `Set.instHasSubset` `dsupport` `Complex` `SchwartzMap` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `SchwartzMap.instFunLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `DFunLike.coe` `TemperedDistribution` `UniformConvergenceCLM.instFunLike` `Complex.instNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `SchwartzMap.instAddCommGroup` `SchwartzMap.instModule` `Complex.instRCLike` `RCLike.innerProductSpace` `SchwartzMap.instTopologicalSpace` `NormedSpace.toModule` `setOf` `Finite` `Set.Elem` `ContinuousLinearMap` `UniformConvergenceCLM.instTopologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `AddCommGroup.toAddCommMonoid` `UniformConvergenceCLM.instAddCommGroup` `UniformConvergenceCLM.instModule` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.funLike` `TemperedDistribution.smulLeftCLM`	—	`dsupport_subset_dsupport` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`dsupport_subset_dsupport` 📖	mathematical	`IsVanishingOn`	`Set` `Set.instHasSubset` `dsupport`	—	`Set.sInter_mono` `IsClosed.isOpen_compl`
`isClosed_dsupport` 📖	mathematical	—	`IsClosed` `dsupport`	—	—
`mem_dsupport_iff` 📖	mathematical	—	`Set` `Set.instMembership` `dsupport`	—	—
`mem_dsupport_iff_forall_exists_ne` 📖	mathematical	—	`Set` `Set.instMembership` `dsupport` `Set.instHasSubset` `tsupport` `DFunLike.coe`	—	—
`mem_dsupport_iff_frequently` 📖	mathematical	—	`Set` `Set.instMembership` `dsupport` `Filter.Frequently` `IsVanishingOn` `Filter.smallSets` `nhds`	—	`Filter.HasBasis.frequently_smallSets` `nhds_basis_opens` `not_isVanishingOn_mono` `mem_dsupport_iff_not_isVanishingOn`
`mem_dsupport_iff_not_isVanishingOn` 📖	mathematical	—	`Set` `Set.instMembership` `dsupport` `IsVanishingOn`	—	—
`notMem_dsupport_iff` 📖	mathematical	—	`Set` `Set.instMembership` `dsupport` `IsVanishingOn` `IsOpen`	—	`dsupport_compl_eq`
`notMem_dsupport_iff_eventually` 📖	mathematical	—	`Set` `Set.instMembership` `dsupport` `Filter.Eventually` `IsVanishingOn` `Filter.smallSets` `nhds`	—	—
`not_isVanishingOn_iff` 📖	mathematical	—	`IsVanishingOn` `Set` `Set.instHasSubset` `tsupport` `DFunLike.coe`	—	—
`not_isVanishingOn_mono` 📖	mathematical	`Set` `Set.instHasSubset` `IsVanishingOn`	`IsVanishingOn`	—	`IsVanishingOn.mono`

Distribution.IsVanishingOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_dsupport` 📖	mathematical	`Distribution.IsVanishingOn` `IsOpen`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Distribution.dsupport`	—	`Set.subset_compl_iff_disjoint_right` `Distribution.dsupport_compl_eq` `Set.subset_sUnion_of_mem`
`iteratedLineDerivOp` 📖	mathematical	`Distribution.IsVanishingOn` `Complex` `SchwartzMap` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `SchwartzMap.instFunLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `DFunLike.coe` `TemperedDistribution` `UniformConvergenceCLM.instFunLike` `Complex.instNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `SchwartzMap.instAddCommGroup` `SchwartzMap.instModule` `Complex.instRCLike` `RCLike.innerProductSpace` `SchwartzMap.instTopologicalSpace` `NormedSpace.toModule` `setOf` `Set` `Finite` `Set.Elem`	`Distribution.IsVanishingOn` `Complex` `SchwartzMap` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `SchwartzMap.instFunLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `DFunLike.coe` `TemperedDistribution` `UniformConvergenceCLM.instFunLike` `Complex.instNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `SchwartzMap.instAddCommGroup` `SchwartzMap.instModule` `Complex.instRCLike` `RCLike.innerProductSpace` `SchwartzMap.instTopologicalSpace` `NormedSpace.toModule` `setOf` `Set` `Finite` `Set.Elem` `LineDeriv.iteratedLineDerivOp` `TemperedDistribution.instLineDeriv`	—	`lineDerivOp`
`lineDerivOp` 📖	mathematical	`Distribution.IsVanishingOn` `Complex` `SchwartzMap` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `SchwartzMap.instFunLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `DFunLike.coe` `TemperedDistribution` `UniformConvergenceCLM.instFunLike` `Complex.instNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `SchwartzMap.instAddCommGroup` `SchwartzMap.instModule` `Complex.instRCLike` `RCLike.innerProductSpace` `SchwartzMap.instTopologicalSpace` `NormedSpace.toModule` `setOf` `Set` `Finite` `Set.Elem`	`Distribution.IsVanishingOn` `Complex` `SchwartzMap` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `SchwartzMap.instFunLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `DFunLike.coe` `TemperedDistribution` `UniformConvergenceCLM.instFunLike` `Complex.instNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `SchwartzMap.instAddCommGroup` `SchwartzMap.instModule` `Complex.instRCLike` `RCLike.innerProductSpace` `SchwartzMap.instTopologicalSpace` `NormedSpace.toModule` `setOf` `Set` `Finite` `Set.Elem` `LineDeriv.lineDerivOp` `TemperedDistribution.instLineDeriv`	—	`map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `UniformConvergenceCLM.instContinuousSemilinearMapClass` `HasSubset.Subset.trans` `Set.instIsTransSubset` `tsupport_fderiv_apply_subset`
`mono` 📖	mathematical	`Set` `Set.instHasSubset` `Distribution.IsVanishingOn`	`Distribution.IsVanishingOn`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset`
`smulLeftCLM` 📖	mathematical	`Distribution.IsVanishingOn` `Complex` `SchwartzMap` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `SchwartzMap.instFunLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `DFunLike.coe` `TemperedDistribution` `UniformConvergenceCLM.instFunLike` `Complex.instNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `SchwartzMap.instAddCommGroup` `SchwartzMap.instModule` `Complex.instRCLike` `RCLike.innerProductSpace` `SchwartzMap.instTopologicalSpace` `NormedSpace.toModule` `setOf` `Set` `Finite` `Set.Elem` `Function.HasTemperateGrowth`	`Distribution.IsVanishingOn` `Complex` `SchwartzMap` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `SchwartzMap.instFunLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `DFunLike.coe` `TemperedDistribution` `UniformConvergenceCLM.instFunLike` `Complex.instNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `SchwartzMap.instAddCommGroup` `SchwartzMap.instModule` `Complex.instRCLike` `RCLike.innerProductSpace` `SchwartzMap.instTopologicalSpace` `NormedSpace.toModule` `setOf` `Set` `Finite` `Set.Elem` `ContinuousLinearMap` `UniformConvergenceCLM.instTopologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `AddCommGroup.toAddCommMonoid` `UniformConvergenceCLM.instAddCommGroup` `UniformConvergenceCLM.instModule` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.funLike` `TemperedDistribution.smulLeftCLM`	—	`IsScalarTower.to_smulCommClass` `Real.isScalarTower` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SchwartzMap.smulLeftCLM_apply` `HasSubset.Subset.trans` `Set.instIsTransSubset` `tsupport_smul_subset_right`

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_dsupport` 📖	mathematical	`Filter.HasBasis` `nhds`	`Set` `Set.instMembership` `Distribution.dsupport` `Distribution.IsVanishingOn`	—	`Distribution.mem_dsupport_iff_frequently` `frequently_smallSets` `Distribution.not_isVanishingOn_mono`
`notMem_dsupport` 📖	mathematical	`Filter.HasBasis` `nhds`	`Set` `Set.instMembership` `Distribution.dsupport` `Distribution.IsVanishingOn`	—	`mem_dsupport`

TemperedDistribution

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isVanishingOn_delta` 📖	mathematical	—	`Distribution.IsVanishingOn` `Complex` `SchwartzMap` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `SchwartzMap.instFunLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex.instZero` `DFunLike.coe` `TemperedDistribution` `Complex.instRCLike` `RCLike.innerProductSpace` `UniformConvergenceCLM.instFunLike` `Complex.instNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `SchwartzMap.instAddCommGroup` `SchwartzMap.instModule` `SchwartzMap.instTopologicalSpace` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `setOf` `Set` `Finite` `Set.Elem` `delta` `Compl.compl` `Set.instCompl` `Set.instSingletonSet`	—	`image_eq_zero_of_notMem_tsupport` `Set.subset_compl_singleton_iff`

---

← Back to Index