Support

📁 Source: Mathlib/Topology/Algebra/Support.lean

Statistics

Metric	Count
Definitions `HasCompactMulSupport`, `HasCompactSupport`, `Support`, `mulTSupport`, `tsupport`	5
Theorems `continuous_of_mulTSupport_subset`, `continuous_of_tsupport_subset`, `comp_homeomorph`, `comp_isClosedEmbedding`, `comp_left`, `comp₂_left`, `continuous_extend_one`, `extend_one`, `intro`, `intro'`, `inv`, `isCompact`, `isCompact_preimage`, `isCompact_range`, `is_one_at_infty`, `mono`, `mono'`, `mul`, `mulTSupport_extend_one`, `mulTSupport_extend_one_subset`, `of_compactSpace`, `of_mulSupport_subset_isCompact`, `one`, `abs`, `add`, `comp_homeomorph`, `comp_isClosedEmbedding`, `comp_left`, `comp₂_left`, `continuous_extend_zero`, `div`, `extend_zero`, `intro`, `intro'`, `isCompact`, `isCompact_preimage`, `isCompact_range`, `is_zero_at_infty`, `mono`, `mono'`, `mul_left`, `mul_right`, `neg`, `of_compactSpace`, `of_support_subset_isCompact`, `smul_left`, `smul_right`, `sub`, `tsupport_extend_zero`, `tsupport_extend_zero_subset`, `zero`, `exists_finset_nhds_mulSupport_subset`, `exists_finset_nhds_support_subset`, `smul_left`, `smul_right`, `continuous_of_mulTSupport`, `continuous_of_tsupport`, `exists_compact_iff_hasCompactMulSupport`, `exists_compact_iff_hasCompactSupport`, `hasCompactMulSupport_comp_left`, `hasCompactMulSupport_def`, `hasCompactMulSupport_iff_eventuallyEq`, `hasCompactSupport_comp_left`, `hasCompactSupport_def`, `hasCompactSupport_iff_eventuallyEq`, `image_eq_one_of_notMem_mulTSupport`, `image_eq_zero_of_notMem_tsupport`, `isClosed_mulTSupport`, `isClosed_tsupport`, `isCompact_range_of_mulSupport_subset_isCompact`, `isCompact_range_of_support_subset_isCompact`, `locallyFinite_mulSupport_iff`, `locallyFinite_support_iff`, `mulTSupport_binop_subset`, `mulTSupport_comp_eq`, `mulTSupport_comp_eq_of_range_subset`, `mulTSupport_comp_eq_preimage`, `mulTSupport_comp_subset`, `mulTSupport_comp_subset_preimage`, `mulTSupport_div`, `mulTSupport_eq_empty_iff`, `mulTSupport_fun_inv`, `mulTSupport_fun_one`, `mulTSupport_inv`, `mulTSupport_mul`, `mulTSupport_mul_inv`, `mulTSupport_one`, `mulTSupport_pow`, `mulTSupport_subset_comp`, `notMem_mulTSupport_iff_eventuallyEq`, `notMem_tsupport_iff_eventuallyEq`, `range_eq_image_mulTSupport_or`, `range_eq_image_tsupport_or`, `range_subset_insert_image_mulTSupport`, `range_subset_insert_image_tsupport`, `subset_mulTSupport`, `subset_tsupport`, `tsupport_add`, `tsupport_add_neg`, `tsupport_binop_subset`, `tsupport_comp_eq`, `tsupport_comp_eq_of_range_subset`, `tsupport_comp_eq_preimage`, `tsupport_comp_subset`, `tsupport_comp_subset_preimage`, `tsupport_eq_empty_iff`, `tsupport_fun_neg`, `tsupport_fun_zero`, `tsupport_mul_subset_left`, `tsupport_mul_subset_right`, `tsupport_neg`, `tsupport_nsmul`, `tsupport_smul_subset_left`, `tsupport_smul_subset_right`, `tsupport_sub`, `tsupport_subset_comp`, `tsupport_zero`	117
Total	122

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_of_mulTSupport_subset` 📖	mathematical	`ContinuousOn` `IsOpen` `Set` `Set.instHasSubset` `mulTSupport`	`Continuous`	—	`continuous_of_mulTSupport` `IsOpen.continuousOn_iff`
`continuous_of_tsupport_subset` 📖	mathematical	`ContinuousOn` `IsOpen` `Set` `Set.instHasSubset` `tsupport`	`Continuous`	—	`continuous_of_tsupport` `IsOpen.continuousOn_iff`

HasCompactMulSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_homeomorph` 📖	mathematical	`HasCompactMulSupport`	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`comp_isClosedEmbedding` `Homeomorph.isClosedEmbedding`
`comp_isClosedEmbedding` 📖	—	`HasCompactMulSupport` `Topology.IsClosedEmbedding`	—	—	`hasCompactMulSupport_def` `Function.mulSupport_comp_eq_preimage` `IsCompact.of_isClosed_subset` `Topology.IsClosedEmbedding.isCompact_preimage` `isClosed_closure` `Topology.IsEmbedding.closure_eq_preimage_closure_image` `Topology.IsClosedEmbedding.isEmbedding` `Set.preimage_mono` `closure_mono` `Set.image_preimage_subset`
`comp_left` 📖	—	`HasCompactMulSupport`	—	—	`mono` `Function.mulSupport_comp_subset`
`comp₂_left` 📖	—	`HasCompactMulSupport`	—	—	`hasCompactMulSupport_iff_eventuallyEq` `Filter.mp_mem` `Filter.univ_mem'`
`continuous_extend_one` 📖	mathematical	`IsOpen` `Continuous` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `HasCompactMulSupport`	`Function.extend` `Pi.instOne`	—	`continuous_of_mulTSupport` `Subtype.coe_image_subset` `mulTSupport_extend_one_subset` `continuous_subtype_val` `Topology.IsOpenEmbedding.continuousAt_iff` `IsOpen.isOpenEmbedding_subtypeVal` `Function.extend_comp` `Subtype.val_injective` `Continuous.continuousAt`
`extend_one` 📖	mathematical	`HasCompactMulSupport` `Continuous`	`Function.extend` `Pi.instOne`	—	`of_mulSupport_subset_isCompact` `T2Space.r1Space` `IsCompact.image` `HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure` `mulTSupport_extend_one_subset`
`intro` 📖	mathematical	`IsCompact`	`HasCompactMulSupport`	—	`exists_compact_iff_hasCompactMulSupport`
`intro'` 📖	mathematical	`IsCompact`	`HasCompactMulSupport`	—	`IsClosed.closure_eq` `closure_mono` `Function.mulSupport_subset_iff'` `IsCompact.of_isClosed_subset` `isClosed_mulTSupport`
`inv` 📖	mathematical	`HasCompactMulSupport` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	`Pi.instInv` `InvOneClass.toInv`	—	`Function.mulSupport_inv`
`isCompact` 📖	mathematical	`HasCompactMulSupport`	`IsCompact` `mulTSupport`	—	—
`isCompact_preimage` 📖	mathematical	`HasCompactMulSupport` `Continuous` `Set` `Set.instMembership`	`IsCompact` `Set.preimage`	—	`IsCompact.of_isClosed_subset` `IsClosed.preimage` `subset_mulTSupport`
`isCompact_range` 📖	mathematical	`HasCompactMulSupport` `Continuous`	`IsCompact` `Set.range`	—	`isCompact_range_of_mulSupport_subset_isCompact` `subset_mulTSupport`
`is_one_at_infty` 📖	mathematical	`HasCompactMulSupport`	`Filter.Tendsto` `Filter.cocompact` `nhds`	—	`Filter.mem_map` `Filter.mem_cocompact'` `isCompact` `Set.compl_subset_comm` `Set.mem_preimage` `image_eq_one_of_notMem_mulTSupport` `mem_of_mem_nhds`
`mono` 📖	—	`HasCompactMulSupport` `Set` `Set.instHasSubset` `Function.mulSupport`	—	—	`mono'` `HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure`
`mono'` 📖	—	`HasCompactMulSupport` `Set` `Set.instHasSubset` `Function.mulSupport` `mulTSupport`	—	—	`IsCompact.of_isClosed_subset` `isClosed_closure` `closure_minimal`
`mul` 📖	mathematical	`HasCompactMulSupport` `MulOne.toOne` `MulOneClass.toMulOne`	`Pi.instMul` `MulOne.toMul`	—	`comp₂_left` `mul_one`
`mulTSupport_extend_one` 📖	mathematical	`HasCompactMulSupport` `Continuous`	`mulTSupport` `Function.extend` `Pi.instOne` `Set.image`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `mulTSupport_extend_one_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `image_closure_subset_closure_image` `closure_mono` `Eq.superset` `Set.instReflSubset` `Function.mulSupport_extend_one`
`mulTSupport_extend_one_subset` 📖	mathematical	`HasCompactMulSupport` `Continuous`	`Set` `Set.instHasSubset` `mulTSupport` `Function.extend` `Pi.instOne` `Set.image`	—	`IsClosed.closure_subset_iff` `IsCompact.isClosed` `IsCompact.image` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Function.mulSupport_extend_one_subset` `Set.image_mono` `subset_closure`
`of_compactSpace` 📖	mathematical	—	`HasCompactMulSupport`	—	`IsCompact.of_isClosed_subset` `isCompact_univ` `isClosed_mulTSupport` `Set.subset_univ`
`of_mulSupport_subset_isCompact` 📖	mathematical	`IsCompact` `Set` `Set.instHasSubset` `Function.mulSupport`	`HasCompactMulSupport`	—	`IsCompact.closure_of_subset`
`one` 📖	mathematical	—	`HasCompactMulSupport` `Pi.instOne`	—	`mulTSupport_one`

HasCompactSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs` 📖	mathematical	`HasCompactSupport` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`abs` `Pi.instLattice` `Pi.addGroup`	—	`comp_left` `abs_zero`
`add` 📖	mathematical	`HasCompactSupport` `AddZero.toZero` `AddZeroClass.toAddZero`	`Pi.instAdd` `AddZero.toAdd`	—	`comp₂_left` `add_zero`
`comp_homeomorph` 📖	mathematical	`HasCompactSupport`	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`comp_isClosedEmbedding` `Homeomorph.isClosedEmbedding`
`comp_isClosedEmbedding` 📖	—	`HasCompactSupport` `Topology.IsClosedEmbedding`	—	—	`hasCompactSupport_def` `Function.support_comp_eq_preimage` `IsCompact.of_isClosed_subset` `Topology.IsClosedEmbedding.isCompact_preimage` `isClosed_closure` `Topology.IsEmbedding.closure_eq_preimage_closure_image` `Topology.IsClosedEmbedding.isEmbedding` `Set.preimage_mono` `closure_mono` `Set.image_preimage_subset`
`comp_left` 📖	—	`HasCompactSupport`	—	—	`mono` `Function.support_comp_subset`
`comp₂_left` 📖	—	`HasCompactSupport`	—	—	`hasCompactSupport_iff_eventuallyEq` `Filter.mp_mem` `Filter.univ_mem'`
`continuous_extend_zero` 📖	mathematical	`IsOpen` `Continuous` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `HasCompactSupport`	`Function.extend` `Pi.instZero`	—	`continuous_of_tsupport` `Subtype.coe_image_subset` `tsupport_extend_zero_subset` `continuous_subtype_val` `Topology.IsOpenEmbedding.continuousAt_iff` `IsOpen.isOpenEmbedding_subtypeVal` `Function.extend_comp` `Subtype.val_injective` `Continuous.continuousAt`
`div` 📖	mathematical	`HasCompactMulSupport` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	`Pi.instDiv` `DivInvMonoid.toDiv` `DivisionMonoid.toDivInvMonoid`	—	`HasCompactMulSupport.mul` `HasCompactMulSupport.inv` `div_eq_mul_inv`
`extend_zero` 📖	mathematical	`HasCompactSupport` `Continuous`	`Function.extend` `Pi.instZero`	—	`of_support_subset_isCompact` `T2Space.r1Space` `IsCompact.image` `HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure` `tsupport_extend_zero_subset`
`intro` 📖	mathematical	`IsCompact`	`HasCompactSupport`	—	`exists_compact_iff_hasCompactSupport`
`intro'` 📖	mathematical	`IsCompact`	`HasCompactSupport`	—	`IsClosed.closure_eq` `closure_mono` `Function.support_subset_iff'` `IsCompact.of_isClosed_subset` `isClosed_tsupport`
`isCompact` 📖	mathematical	`HasCompactSupport`	`IsCompact` `tsupport`	—	—
`isCompact_preimage` 📖	mathematical	`HasCompactSupport` `Continuous` `Set` `Set.instMembership`	`IsCompact` `Set.preimage`	—	`IsCompact.of_isClosed_subset` `IsClosed.preimage` `subset_tsupport` `Function.mem_support` `Set.mem_preimage`
`isCompact_range` 📖	mathematical	`HasCompactSupport` `Continuous`	`IsCompact` `Set.range`	—	`isCompact_range_of_support_subset_isCompact` `subset_tsupport`
`is_zero_at_infty` 📖	mathematical	`HasCompactSupport`	`Filter.Tendsto` `Filter.cocompact` `nhds`	—	`Filter.mem_map` `Filter.mem_cocompact'` `isCompact` `Set.compl_subset_comm` `Set.mem_preimage` `image_eq_zero_of_notMem_tsupport` `mem_of_mem_nhds`
`mono` 📖	—	`HasCompactSupport` `Set` `Set.instHasSubset` `Function.support`	—	—	`mono'` `HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure`
`mono'` 📖	—	`HasCompactSupport` `Set` `Set.instHasSubset` `Function.support` `tsupport`	—	—	`IsCompact.of_isClosed_subset` `isClosed_closure` `closure_minimal`
`mul_left` 📖	mathematical	`HasCompactSupport` `MulZeroClass.toZero`	`Pi.instMul` `MulZeroClass.toMul`	—	`hasCompactSupport_iff_eventuallyEq` `Filter.Eventually.mono` `MulZeroClass.mul_zero`
`mul_right` 📖	mathematical	`HasCompactSupport` `MulZeroClass.toZero`	`Pi.instMul` `MulZeroClass.toMul`	—	`hasCompactSupport_iff_eventuallyEq` `Filter.Eventually.mono` `MulZeroClass.zero_mul`
`neg` 📖	mathematical	`HasCompactSupport` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	`Pi.instNeg` `NegZeroClass.toNeg`	—	`Function.support_neg`
`of_compactSpace` 📖	mathematical	—	`HasCompactSupport`	—	`IsCompact.of_isClosed_subset` `isCompact_univ` `isClosed_tsupport` `Set.subset_univ`
`of_support_subset_isCompact` 📖	mathematical	`IsCompact` `Set` `Set.instHasSubset` `Function.support`	`HasCompactSupport`	—	`IsCompact.closure_of_subset`
`smul_left` 📖	mathematical	`HasCompactSupport`	`Pi.smul'` `SMulZeroClass.toSMul`	—	`hasCompactSupport_iff_eventuallyEq` `Filter.Eventually.mono` `smul_zero`
`smul_right` 📖	mathematical	`HasCompactSupport`	`Pi.smul'` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	—	`hasCompactSupport_iff_eventuallyEq` `Filter.Eventually.mono` `zero_smul`
`sub` 📖	mathematical	`HasCompactSupport` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	`Pi.instSub` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid`	—	`add` `neg` `sub_eq_add_neg`
`tsupport_extend_zero` 📖	mathematical	`HasCompactSupport` `Continuous`	`tsupport` `Function.extend` `Pi.instZero` `Set.image`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `tsupport_extend_zero_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `image_closure_subset_closure_image` `closure_mono` `Eq.superset` `Set.instReflSubset` `Function.support_extend_zero`
`tsupport_extend_zero_subset` 📖	mathematical	`HasCompactSupport` `Continuous`	`Set` `Set.instHasSubset` `tsupport` `Function.extend` `Pi.instZero` `Set.image`	—	`IsClosed.closure_subset_iff` `IsCompact.isClosed` `IsCompact.image` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Function.support_extend_zero_subset` `Set.image_mono` `subset_closure`
`zero` 📖	mathematical	—	`HasCompactSupport` `Pi.instZero`	—	`tsupport_zero` `Set.Finite.isCompact` `Set.finite_empty`

IsDedekindDomain.HeightOneSpectrum

Definitions

Name	Category	Theorems
`Support` 📖	CompOp	1 math math: `Support.finite`

LocallyFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_finset_nhds_mulSupport_subset` 📖	mathematical	`LocallyFinite` `Function.mulSupport` `Set` `Set.instHasSubset` `mulTSupport` `IsOpen`	`Filter` `Filter.instMembership` `nhds` `Set.iInter` `Finset` `Finset.instMembership` `SetLike.coe` `Finset.instSetLike`	—	`Filter.inter_mem` `Filter.biInter_finset_mem` `IsClosed.compl_mem_nhds` `isClosed_mulTSupport` `Set.notMem_subset` `Finset.mem_filter` `IsOpen.mem_nhds` `Set.inter_subset_right` `Set.mem_of_mem_inter_left` `Set.inter_assoc` `Set.mem_of_mem_inter_right` `Set.Finite.coe_toFinset` `Finset.subset_coe_filter_of_subset_forall` `Mathlib.Tactic.Contrapose.contrapose₁` `subset_mulTSupport` `Set.iInter_congr_Prop`
`exists_finset_nhds_support_subset` 📖	mathematical	`LocallyFinite` `Function.support` `Set` `Set.instHasSubset` `tsupport` `IsOpen`	`Filter` `Filter.instMembership` `nhds` `Set.iInter` `Finset` `Finset.instMembership` `SetLike.coe` `Finset.instSetLike`	—	`Filter.inter_mem` `Filter.biInter_finset_mem` `IsClosed.compl_mem_nhds` `isClosed_tsupport` `Set.notMem_subset` `Finset.mem_filter` `IsOpen.mem_nhds` `Set.inter_subset_right` `Set.mem_of_mem_inter_left` `Set.inter_assoc` `Set.mem_of_mem_inter_right` `Set.Finite.coe_toFinset` `Finset.subset_coe_filter_of_subset_forall` `Mathlib.Tactic.Contrapose.contrapose₁` `Set.mem_compl_iff` `subset_tsupport` `Set.iInter_congr_Prop` `Set.Finite.mem_toFinset` `Set.mem_iInter`
`smul_left` 📖	mathematical	`LocallyFinite` `Function.support`	`Pi.smul'` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	—	`subset` `Pi.smul_apply'` `zero_smul`
`smul_right` 📖	mathematical	`LocallyFinite` `Function.support`	`Pi.smul'` `SMulZeroClass.toSMul`	—	`subset` `Pi.smul_apply'` `smul_zero`

(root)

Definitions

Name	Category	Theorems
`HasCompactMulSupport` 📖	MathDef	9 math math: `hasCompactMulSupport_def`, `HasCompactMulSupport.of_mulSupport_subset_isCompact`, `HasCompactMulSupport.of_compactSpace`, `HasCompactMulSupport.one`, `hasCompactMulSupport_comp_left`, `hasCompactMulSupport_iff_eventuallyEq`, `HasCompactMulSupport.intro'`, `exists_compact_iff_hasCompactMulSupport`, `HasCompactMulSupport.intro`
`HasCompactSupport` 📖	MathDef	42 math math: `exists_continuous_sum_one_of_isOpen_isCompact`, `HasCompactSupport.intro`, `HasCompactSupport.of_support_subset_isCompact`, `CompactlySupportedContinuousMap.hasCompactSupport`, `MeasureTheory.Integrable.exists_hasCompactSupport_lintegral_sub_le`, `exists_smooth_tsupport_subset`, `MeasureTheory.MemLp.exist_eLpNorm_sub_le`, `hasCompactSupport_iff_eventuallyEq`, `ExistsContDiffBumpBase.w_compact_support`, `CompactlySupportedContinuousMapClass.hasCompactSupport`, `ContDiffBump.hasCompactSupport`, `ContDiffMapSupportedIn.hasCompactSupport`, `MeasureTheory.Measure.innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_group`, `SmoothBumpFunction.hasCompactSupport`, `exists_continuous_one_zero_of_isCompact`, `exists_continuous_nonneg_pos`, `PartitionOfUnity.exists_isSubordinate_of_locallyFinite_t2space`, `MeasureTheory.Integrable.exists_hasCompactSupport_integral_sub_le`, `TestFunctionClass.map_hasCompactSupport`, `MeasureTheory.MemLp.exists_hasCompactSupport_integral_rpow_sub_le`, `mem_compactlySupported`, `HasCompactSupport.intro'`, `MeasureTheory.MemLp.exists_hasCompactSupport_eLpNorm_sub_le`, `exists_compact_iff_hasCompactSupport`, `hasCompactSupport_def`, `BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop_t2space`, `TestFunction.hasCompactSupport'`, `CompactlySupportedContinuousMap.hasCompactSupport'`, `exists_continuous_one_zero_of_isCompact_of_isGδ`, `HasCompactSupport.of_compactSpace`, `ContDiffBump.hasCompactSupport_normed`, `IsCompact.measure_eq_biInf_integral_hasCompactSupport`, `TestFunction.hasCompactSupport`, `HasCompactSupport.zero`, `exists_contDiff_tsupport_subset`, `ExistsContDiffBumpBase.u_compact_support`, `MeasureTheory.Lp.dense_hasCompactSupport_contDiff`, `hasCompactSupport_norm_iff`, `ContDiffMapSupportedIn.compact_supp`, `MeasureTheory.Measure.innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_addGroup`, `BumpCovering.exists_isSubordinate_hasCompactSupport_of_locallyFinite_t2space`, `hasCompactSupport_comp_left`
`mulTSupport` 📖	CompOp	25 math math: `mulTSupport_mul_inv`, `mulTSupport_eq_empty_iff`, `HasCompactMulSupport.mulTSupport_extend_one_subset`, `subset_mulTSupport`, `mulTSupport_mul`, `HasCompactMulSupport.mulTSupport_extend_one`, `range_eq_image_mulTSupport_or`, `HasCompactMulSupport.isCompact`, `mulTSupport_binop_subset`, `mulTSupport_fun_inv`, `range_subset_insert_image_mulTSupport`, `isClosed_mulTSupport`, `mulTSupport_subset_comp`, `mulTSupport_comp_subset_preimage`, `mulTSupport_comp_eq_of_range_subset`, `mulTSupport_fun_one`, `mulTSupport_comp_subset`, `mulTSupport_pow`, `mulTSupport_comp_eq_preimage`, `mulTSupport_inv`, `mulTSupport_comp_eq`, `mulTSupport_one`, `mulTSupport_div`, `notMem_mulTSupport_iff_eventuallyEq`, `locallyFinite_mulSupport_iff`
`tsupport` 📖	CompOp	67 math math: `exists_continuous_sum_one_of_isOpen_isCompact`, `HasCompactSupport.convolution_integrand_bound_left`, `tsupport_binop_subset`, `tsupport_fun_zero`, `exists_smooth_tsupport_subset`, `subset_tsupport`, `tsupport_neg`, `tsupport_comp_eq`, `SmoothBumpFunction.tsupport_subset_symm_image_closedBall`, `SmoothBumpFunction.tsupport_subset_chartAt_source`, `SchwartzMap.tsupport_lineDerivOp_subset`, `MeasureTheory.setIntegral_tsupport`, `tsupport_comp_eq_of_range_subset`, `SmoothBumpFunction.tsupport_mem_nhds`, `tsupport_mul_subset_left`, `SmoothBumpFunction.nhds_basis_support`, `ContDiffMapSupportedIn.tsupport_subset`, `support_deriv_subset`, `notMem_tsupport_iff_eventuallyEq`, `SchwartzMap.tsupport_iteratedLineDerivOp_subset`, `PartitionOfUnity.locallyFinite_tsupport`, `BumpCovering.locallyFinite_tsupport`, `HasCompactSupport.isCompact`, `locallyFinite_support_iff`, `tsupport_comp_subset_preimage`, `tsupport_nsmul`, `HasCompactSupport.tsupport_extend_zero_subset`, `TestFunction.tsupport_subset`, `isClosed_tsupport`, `support_iteratedFDeriv_subset`, `SchwartzMap.tsupport_smulLeftCLM_subset`, `tsupport_fderiv_subset`, `SchwartzMap.tsupport_fderivCLM_subset`, `tsupport_iteratedFDeriv_subset`, `range_eq_image_tsupport_or`, `ContDiffBump.tsupport_eq`, `tsupport_comp_eq_preimage`, `tsupport_subset_comp`, `tsupport_fun_neg`, `tsupport_fderiv_apply_subset`, `exists_continuousMap_one_of_isCompact_subset_isOpen`, `tsupport_comp_subset`, `SmoothPartitionOfUnity.finite_tsupport`, `tsupport_smul_subset_right`, `SmoothBumpFunction.tsupport_subset_extChartAt_source`, `SchwartzMap.tsupport_derivCLM_subset`, `SmoothPartitionOfUnity.mem_fintsupport_iff`, `HasCompactSupport.tsupport_extend_zero`, `PartitionOfUnity.finite_tsupport`, `tsupport_add`, `exists_contDiff_tsupport_subset`, `tsupport_mul_subset_right`, `PartitionOfUnity.mem_fintsupport_iff`, `RealRMK.range_cut_partition`, `ContDiffBump.tsupport_normed_eq`, `exists_tsupport_one_of_isOpen_isClosed`, `TestFunctionClass.tsupport_map_subset`, `support_fderiv_subset`, `TestFunction.tsupport_subset'`, `tsupport_zero`, `tsupport_sub`, `SmoothBumpFunction.nhds_basis_tsupport`, `HasCompactSupport.convolution_integrand_bound_right`, `tsupport_add_neg`, `tsupport_eq_empty_iff`, `tsupport_smul_subset_left`, `range_subset_insert_image_tsupport`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_of_mulTSupport` 📖	mathematical	`ContinuousAt`	`Continuous`	—	`continuous_iff_continuousAt` `em` `ContinuousAt.congr` `continuousAt_const` `Filter.EventuallyEq.symm` `notMem_mulTSupport_iff_eventuallyEq`
`continuous_of_tsupport` 📖	mathematical	`ContinuousAt`	`Continuous`	—	`continuous_iff_continuousAt` `em` `ContinuousAt.congr` `continuousAt_const` `Filter.EventuallyEq.symm` `notMem_tsupport_iff_eventuallyEq`
`exists_compact_iff_hasCompactMulSupport` 📖	mathematical	—	`IsCompact` `HasCompactMulSupport`	—	—
`exists_compact_iff_hasCompactSupport` 📖	mathematical	—	`IsCompact` `HasCompactSupport`	—	`Function.notMem_support` `Set.mem_compl_iff` `Set.compl_subset_compl` `hasCompactSupport_def` `exists_isCompact_superset_iff`
`hasCompactMulSupport_comp_left` 📖	mathematical	—	`HasCompactMulSupport`	—	`Function.mulSupport_comp_eq`
`hasCompactMulSupport_def` 📖	mathematical	—	`HasCompactMulSupport` `IsCompact` `closure` `Function.mulSupport`	—	—
`hasCompactMulSupport_iff_eventuallyEq` 📖	mathematical	—	`HasCompactMulSupport` `Filter.EventuallyEq` `Filter.coclosedCompact` `Pi.instOne`	—	`Filter.mem_coclosedCompact_iff`
`hasCompactSupport_comp_left` 📖	mathematical	—	`HasCompactSupport`	—	`hasCompactSupport_def` `Function.support_comp_eq`
`hasCompactSupport_def` 📖	mathematical	—	`HasCompactSupport` `IsCompact` `closure` `Function.support`	—	—
`hasCompactSupport_iff_eventuallyEq` 📖	mathematical	—	`HasCompactSupport` `Filter.EventuallyEq` `Filter.coclosedCompact` `Pi.instZero`	—	`Filter.mem_coclosedCompact_iff`
`image_eq_one_of_notMem_mulTSupport` 📖	—	`Set` `Set.instMembership` `mulTSupport`	—	—	`Function.mulSupport_subset_iff'` `subset_mulTSupport`
`image_eq_zero_of_notMem_tsupport` 📖	—	`Set` `Set.instMembership` `tsupport`	—	—	`Function.support_subset_iff'` `subset_tsupport`
`isClosed_mulTSupport` 📖	mathematical	—	`IsClosed` `mulTSupport`	—	`isClosed_closure`
`isClosed_tsupport` 📖	mathematical	—	`IsClosed` `tsupport`	—	`isClosed_closure`
`isCompact_range_of_mulSupport_subset_isCompact` 📖	mathematical	`Continuous` `IsCompact` `Set` `Set.instHasSubset` `Function.mulSupport`	`Set.range`	—	`Function.range_eq_image_or_of_mulSupport_subset` `IsCompact.image` `IsCompact.insert`
`isCompact_range_of_support_subset_isCompact` 📖	mathematical	`Continuous` `IsCompact` `Set` `Set.instHasSubset` `Function.support`	`Set.range`	—	`Function.range_eq_image_or_of_support_subset` `IsCompact.image` `IsCompact.insert`
`locallyFinite_mulSupport_iff` 📖	mathematical	—	`LocallyFinite` `Function.mulSupport` `mulTSupport`	—	`LocallyFinite.closure` `LocallyFinite.subset` `subset_closure`
`locallyFinite_support_iff` 📖	mathematical	—	`LocallyFinite` `Function.support` `tsupport`	—	`LocallyFinite.closure` `LocallyFinite.subset` `subset_closure`
`mulTSupport_binop_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `mulTSupport` `Set.instUnion`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `closure_mono` `Function.mulSupport_binop_subset` `Eq.subset` `Set.instReflSubset` `closure_union`
`mulTSupport_comp_eq` 📖	mathematical	—	`mulTSupport`	—	`mulTSupport.eq_1` `Function.mulSupport_comp_eq`
`mulTSupport_comp_eq_of_range_subset` 📖	mathematical	—	`mulTSupport`	—	`mulTSupport.eq_1` `Function.mulSupport_comp_eq_of_range_subset`
`mulTSupport_comp_eq_preimage` 📖	mathematical	—	`mulTSupport` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Set.preimage`	—	`mulTSupport.eq_1` `Function.mulSupport_comp_eq_preimage` `Homeomorph.preimage_closure`
`mulTSupport_comp_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `mulTSupport`	—	`closure_mono` `Function.mulSupport_comp_subset`
`mulTSupport_comp_subset_preimage` 📖	mathematical	`Continuous`	`Set` `Set.instHasSubset` `mulTSupport` `Set.preimage`	—	`mulTSupport.eq_1` `Function.mulSupport_comp_eq_preimage` `Continuous.closure_preimage_subset`
`mulTSupport_div` 📖	mathematical	—	`Set` `Set.instHasSubset` `mulTSupport` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivInvMonoid.toDiv` `DivisionMonoid.toDivInvMonoid` `Set.instUnion`	—	`mulTSupport_binop_subset` `one_div_one`
`mulTSupport_eq_empty_iff` 📖	mathematical	—	`mulTSupport` `Set` `Set.instEmptyCollection` `Pi.instOne`	—	`mulTSupport.eq_1` `closure_empty_iff` `Function.mulSupport_eq_empty_iff`
`mulTSupport_fun_inv` 📖	mathematical	—	`mulTSupport` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `InvOneClass.toInv`	—	`Function.mulSupport_fun_inv`
`mulTSupport_fun_one` 📖	mathematical	—	`mulTSupport` `Set` `Set.instEmptyCollection`	—	`mulTSupport.eq_1` `Function.mulSupport_fun_one` `closure_empty`
`mulTSupport_inv` 📖	mathematical	—	`mulTSupport` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Pi.instInv` `InvOneClass.toInv`	—	`mulTSupport_fun_inv`
`mulTSupport_mul` 📖	mathematical	—	`Set` `Set.instHasSubset` `mulTSupport` `MulOne.toOne` `MulOneClass.toMulOne` `MulOne.toMul` `Set.instUnion`	—	`mulTSupport_binop_subset` `mul_one`
`mulTSupport_mul_inv` 📖	mathematical	—	`Set` `Set.instHasSubset` `mulTSupport` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid` `InvOneClass.toInv` `Set.instUnion`	—	`mulTSupport_binop_subset` `inv_one` `mul_one`
`mulTSupport_one` 📖	mathematical	—	`mulTSupport` `Pi.instOne` `Set` `Set.instEmptyCollection`	—	`mulTSupport.eq_1` `Function.mulSupport_one` `closure_empty`
`mulTSupport_pow` 📖	mathematical	—	`Set` `Set.instHasSubset` `mulTSupport` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toNatPow`	—	`closure_mono` `Function.mulSupport_pow`
`mulTSupport_subset_comp` 📖	mathematical	—	`Set` `Set.instHasSubset` `mulTSupport`	—	`closure_mono` `Function.mulSupport_subset_comp`
`notMem_mulTSupport_iff_eventuallyEq` 📖	mathematical	—	`Set` `Set.instMembership` `mulTSupport` `Filter.EventuallyEq` `nhds` `Pi.instOne`	—	—
`notMem_tsupport_iff_eventuallyEq` 📖	mathematical	—	`Set` `Set.instMembership` `tsupport` `Filter.EventuallyEq` `nhds` `Pi.instZero`	—	`mem_closure_iff_nhds` `Set.not_nonempty_iff_eq_empty` `Set.disjoint_iff_inter_eq_empty` `Function.disjoint_support_iff` `Filter.eventuallyEq_iff_exists_mem`
`range_eq_image_mulTSupport_or` 📖	mathematical	—	`Set.range` `Set.image` `mulTSupport` `Set` `Set.instInsert`	—	`WCovBy.eq_or_eq` `Set.wcovBy_insert` `Set.image_subset_range` `range_subset_insert_image_mulTSupport`
`range_eq_image_tsupport_or` 📖	mathematical	—	`Set.range` `Set.image` `tsupport` `Set` `Set.instInsert`	—	`WCovBy.eq_or_eq` `Set.wcovBy_insert` `Set.image_subset_range` `range_subset_insert_image_tsupport`
`range_subset_insert_image_mulTSupport` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.range` `Set.instInsert` `Set.image` `mulTSupport`	—	`Mathlib.Tactic.GCongr.rel_imp_rel` `Set.instIsTransSubset` `subset_refl` `Set.instReflSubset` `Set.insert_subset_insert` `Set.image_mono` `subset_mulTSupport` `Function.range_subset_insert_image_mulSupport`
`range_subset_insert_image_tsupport` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.range` `Set.instInsert` `Set.image` `tsupport`	—	`Mathlib.Tactic.GCongr.rel_imp_rel` `Set.instIsTransSubset` `subset_refl` `Set.instReflSubset` `Set.insert_subset_insert` `Set.image_mono` `subset_tsupport` `Function.range_subset_insert_image_support`
`subset_mulTSupport` 📖	mathematical	—	`Set` `Set.instHasSubset` `Function.mulSupport` `mulTSupport`	—	`subset_closure`
`subset_tsupport` 📖	mathematical	—	`Set` `Set.instHasSubset` `Function.support` `tsupport`	—	`subset_closure`
`tsupport_add` 📖	mathematical	—	`Set` `Set.instHasSubset` `tsupport` `AddZero.toZero` `AddZeroClass.toAddZero` `AddZero.toAdd` `Set.instUnion`	—	`tsupport_binop_subset` `add_zero`
`tsupport_add_neg` 📖	mathematical	—	`Set` `Set.instHasSubset` `tsupport` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid` `NegZeroClass.toNeg` `Set.instUnion`	—	`tsupport_binop_subset` `neg_zero` `add_zero`
`tsupport_binop_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `tsupport` `Set.instUnion`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `closure_mono` `Function.support_binop_subset` `Eq.subset` `Set.instReflSubset` `closure_union`
`tsupport_comp_eq` 📖	mathematical	—	`tsupport`	—	`tsupport.eq_1` `Function.support_comp_eq`
`tsupport_comp_eq_of_range_subset` 📖	mathematical	—	`tsupport`	—	`tsupport.eq_1` `Function.support_comp_eq_of_range_subset`
`tsupport_comp_eq_preimage` 📖	mathematical	—	`tsupport` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Set.preimage`	—	`tsupport.eq_1` `Function.support_comp_eq_preimage` `Homeomorph.preimage_closure`
`tsupport_comp_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `tsupport`	—	`closure_mono` `Function.support_comp_subset`
`tsupport_comp_subset_preimage` 📖	mathematical	`Continuous`	`Set` `Set.instHasSubset` `tsupport` `Set.preimage`	—	`tsupport.eq_1` `Function.support_comp_eq_preimage` `Continuous.closure_preimage_subset`
`tsupport_eq_empty_iff` 📖	mathematical	—	`tsupport` `Set` `Set.instEmptyCollection` `Pi.instZero`	—	`tsupport.eq_1` `closure_empty_iff` `Function.support_eq_empty_iff`
`tsupport_fun_neg` 📖	mathematical	—	`tsupport` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `NegZeroClass.toNeg`	—	`Function.support_fun_neg`
`tsupport_fun_zero` 📖	mathematical	—	`tsupport` `Set` `Set.instEmptyCollection`	—	`tsupport.eq_1` `Function.support_fun_zero` `closure_empty`
`tsupport_mul_subset_left` 📖	mathematical	—	`Set` `Set.instHasSubset` `tsupport` `MulZeroClass.toZero` `MulZeroClass.toMul`	—	`closure_mono` `Function.support_mul_subset_left`
`tsupport_mul_subset_right` 📖	mathematical	—	`Set` `Set.instHasSubset` `tsupport` `MulZeroClass.toZero` `MulZeroClass.toMul`	—	`closure_mono` `Function.support_mul_subset_right`
`tsupport_neg` 📖	mathematical	—	`tsupport` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `Pi.instNeg` `NegZeroClass.toNeg`	—	`tsupport_fun_neg`
`tsupport_nsmul` 📖	mathematical	—	`Set` `Set.instHasSubset` `tsupport` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNatSMul`	—	`closure_mono` `Function.support_nsmul`
`tsupport_smul_subset_left` 📖	mathematical	—	`Set` `Set.instHasSubset` `tsupport` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass`	—	`closure_mono` `Function.support_smul_subset_left`
`tsupport_smul_subset_right` 📖	mathematical	—	`Set` `Set.instHasSubset` `tsupport` `SMulZeroClass.toSMul`	—	`closure_mono` `Function.support_smul_subset_right`
`tsupport_sub` 📖	mathematical	—	`Set` `Set.instHasSubset` `tsupport` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid` `Set.instUnion`	—	`tsupport_binop_subset` `zero_sub_zero`
`tsupport_subset_comp` 📖	mathematical	—	`Set` `Set.instHasSubset` `tsupport`	—	`closure_mono` `Function.support_subset_comp`
`tsupport_zero` 📖	mathematical	—	`tsupport` `Pi.instZero` `Set` `Set.instEmptyCollection`	—	`tsupport.eq_1` `Function.support_zero` `closure_empty`

---

← Back to Index