LocallyFinsupp

📁 Source: Mathlib/Topology/LocallyFinsupp.lean

Statistics

Metric	Count
Definitions locallyFinsupp, locallyFinsuppWithin, addSubgroup, addSubmonoid, instAdd, instAddCommGroup, instAddCommMonoid, instAddGroup, instAddMonoid, instFunLike, instLE, instLTOfPreorder, instLattice, instMaxOfSemilatticeSup, instMinOfSemilatticeInf, instNeg, instSMulInt, instSMulNat, instSub, instZero, mk_of_mem, mk_of_mem_addSubgroup, mk_of_mem_addSubmonoid, restrict, restrictLatticeHom, restrictMonoidHom, single, support, toFun, LocallyFiniteSupport, instZeroLocallyFinsuppWithin	31
Theorems locallyFiniteSupport, apply_eq_zero_of_notMem, closedSupport, coe_add, coe_finsum, coe_injective, coe_neg, coe_nsmul, coe_single, coe_sub, coe_sum, coe_zero, coe_zsmul, discreteSupport, eq_zero_codiscreteWithin, exists_single_le_pos, ext, ext_iff, finiteSupport, instIsOrderedAddMonoid, le_def, lt_def, max_apply, memAddSubgroup, memAddSubmonoid, min_apply, mk_of_mem_addSubgroup_toFun, mk_of_mem_addSubmonoid_toFun, negPart_add, negPart_apply, nsmul_negPart, nsmul_posPart, posPart_add, posPart_apply, restrictLatticeHom_apply, restrictMonoidHom_apply, restrict_apply, restrict_eqOn, restrict_eqOn_compl, restrict_negPart, restrict_posPart, restrict_zero, single_apply, single_nonneg, single_pos, single_pos_int_one, single_pos_nat_one, single_zero, sum_apply_smul_single_eq_self, supportLocallyFiniteWithinDomain, supportLocallyFiniteWithinDomain', supportWithinDomain, supportWithinDomain', finite_inter_support_of_isCompact, iff_locallyFinite_support, locallyFinite_support, supportDiscreteWithin_iff_locallyFiniteWithin	57
Total	88

Function

Definitions

Name	Category	Theorems
locallyFinsupp 📖	CompOp	29 math math: ValueDistribution.logCounting_zero, locallyFinsuppWithin.logCounting_single_eq_log_sub_const, locallyFinsuppWithin.logCounting_strictMono, locallyFinsuppWithin.toClosedBall_support_subset_closedBall, locallyFinsuppWithin.zero_iff_logCounting_bounded, locallyFinsuppWithin.logCounting_nonneg, locallyFinsuppWithin.single_zero, locallyFinsuppWithin.logCounting_eval_zero, ValueDistribution.logCounting_top, locallyFinsuppWithin.logCounting_eventually_le, locallyFinsuppWithin.logCounting_eventuallyLE, locallyFinsuppWithin.toClosedBall_divisor, locallyFinsuppWithin.single_apply, locallyFinsuppWithin.single_pos, locallyFinsuppWithin.exists_single_le_pos, locallyFinsuppWithin.coe_single, ValueDistribution.characteristic_sub_characteristic_inv, locallyFinsuppWithin.single_nonneg, locallyFinsuppWithin.logCounting_divisor, locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const, locallyFinsuppWithin.logCounting_mono, locallyFinsuppWithin.logCounting_le, locallyFinsuppWithin.one_isLittleO_logCounting_single, ValueDistribution.logCounting_coe, ValueDistribution.log_counting_zero_sub_logCounting_top, locallyFinsuppWithin.single_pos_int_one, locallyFinsuppWithin.single_pos_nat_one, locallyFinsuppWithin.logCounting_even, locallyFinsuppWithin.toClosedBall_eval_within
locallyFinsuppWithin 📖	CompData	79 math math: ValueDistribution.logCounting_zero, FactorizedRational.divisor, locallyFinsuppWithin.toClosedBall_support_subset_closedBall, MeromorphicOn.divisor_fun_smul, AnalyticOnNhd.circleAverage_log_norm, MeromorphicOn.divisor_const, locallyFinsuppWithin.zero_iff_logCounting_bounded, MeromorphicOn.divisor_pow, locallyFinsuppWithin.restrict_apply, MeromorphicOn.extract_zeros_poles_log, MeromorphicOn.divisor_natCast, locallyFinsuppWithin.nsmul_posPart, ValueDistribution.logCounting_top, locallyFinsuppWithin.apply_eq_zero_of_notMem, MeromorphicOn.divisor_inv, MeromorphicOn.divisor_fun_pow, MeromorphicOn.divisor_fun_prod, locallyFinsuppWithin.posPart_add, locallyFinsuppWithin.eq_zero_codiscreteWithin, MeromorphicOn.divisor_sub_const_self, MeromorphicOn.divisor_prod, MeromorphicOn.divisor_intCast, locallyFinsuppWithin.instIsOrderedAddMonoid, locallyFinsuppWithin.le_def, locallyFinsuppWithin.coe_sub, locallyFinsuppWithin.restrict_zero, MeromorphicOn.divisor_sub_const_of_ne, locallyFinsuppWithin.ext_iff, MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_right, locallyFinsuppWithin.restrict_eqOn_compl, locallyFinsuppWithin.coe_zsmul, locallyFinsuppWithin.toClosedBall_divisor, MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_left, MeromorphicOn.divisor_ofNat, locallyFinsuppWithin.coe_sum, locallyFinsuppWithin.memAddSubmonoid, MeromorphicOn.divisor_fun_zpow, MeromorphicOn.divisor_apply, MeromorphicOn.divisor_fun_mul, MeromorphicOn.divisor_zpow, locallyFinsuppWithin.restrict_eqOn, MeromorphicNFOn.divisor_nonneg_iff_analyticOnNhd, locallyFinsuppWithin.negPart_add, locallyFinsuppWithin.mk_of_mem_addSubmonoid_toFun, MeromorphicOn.divisor_fun_inv, MeromorphicNFOn.zero_set_eq_divisor_support, MeromorphicOn.circleAverage_log_norm, locallyFinsuppWithin.coe_nsmul, MeromorphicOn.AnalyticOnNhd.divisor_nonneg, locallyFinsuppWithin.posPart_apply, locallyFinsuppWithin.mk_of_mem_addSubgroup_toFun, circleAverage_log_norm_factorizedRational, MeromorphicOn.min_divisor_le_divisor_add, locallyFinsuppWithin.restrict_posPart, MeromorphicOn.extract_zeros_poles, AnalyticOnNhd.sum_divisor_le, MeromorphicOn.negPart_divisor_add_le_max, locallyFinsuppWithin.restrictMonoidHom_apply, locallyFinsuppWithin.sum_apply_smul_single_eq_self, MeromorphicOn.divisor_smul, locallyFinsuppWithin.nsmul_negPart, locallyFinsuppWithin.coe_add, MeromorphicOn.negPart_divisor_add_le_add, MeromorphicOn.AnalyticOnNhd.divisor_apply, locallyFinsuppWithin.restrictLatticeHom_apply, MeromorphicOn.divisor_def, locallyFinsuppWithin.restrict_negPart, locallyFinsuppWithin.coe_zero, locallyFinsuppWithin.negPart_apply, ValueDistribution.logCounting_coe, locallyFinsuppWithin.coe_injective, locallyFinsuppWithin.coe_finsum, locallyFinsuppWithin.coe_neg, locallyFinsuppWithin.min_apply, MeromorphicOn.divisor_mul, locallyFinsuppWithin.max_apply, locallyFinsuppWithin.lt_def, locallyFinsuppWithin.memAddSubgroup, locallyFinsuppWithin.toClosedBall_eval_within

Function.locallyFinsupp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallyFiniteSupport 📖	mathematical	—	LocallyFiniteSupport Function.locallyFinsuppWithin.toFun Set.univ	—	Function.locallyFinsuppWithin.supportLocallyFiniteWithinDomain'

Function.locallyFinsuppWithin

Definitions

Name	Category	Theorems
addSubgroup 📖	CompOp	1 math math: memAddSubgroup
addSubmonoid 📖	CompOp	1 math math: memAddSubmonoid
instAdd 📖	CompOp	8 math math: MeromorphicOn.divisor_fun_smul, posPart_add, MeromorphicOn.divisor_fun_mul, negPart_add, MeromorphicOn.divisor_smul, coe_add, MeromorphicOn.negPart_divisor_add_le_add, MeromorphicOn.divisor_mul
instAddCommGroup 📖	CompOp	—
instAddCommMonoid 📖	CompOp	6 math math: MeromorphicOn.divisor_fun_prod, MeromorphicOn.divisor_prod, instIsOrderedAddMonoid, coe_sum, sum_apply_smul_single_eq_self, coe_finsum
instAddGroup 📖	CompOp	15 math math: ValueDistribution.logCounting_zero, nsmul_posPart, ValueDistribution.logCounting_top, posPart_add, MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_right, MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_left, negPart_add, posPart_apply, restrict_posPart, MeromorphicOn.negPart_divisor_add_le_max, nsmul_negPart, MeromorphicOn.negPart_divisor_add_le_add, restrict_negPart, negPart_apply, ValueDistribution.logCounting_coe
instAddMonoid 📖	CompOp	22 math math: ValueDistribution.logCounting_zero, logCounting_single_eq_log_sub_const, logCounting_strictMono, toClosedBall_support_subset_closedBall, zero_iff_logCounting_bounded, logCounting_nonneg, logCounting_eval_zero, ValueDistribution.logCounting_top, logCounting_eventually_le, logCounting_eventuallyLE, toClosedBall_divisor, ValueDistribution.characteristic_sub_characteristic_inv, locallyFinsuppWithin.logCounting_divisor, logCounting_divisor_eq_circleAverage_sub_const, restrictMonoidHom_apply, logCounting_mono, logCounting_le, one_isLittleO_logCounting_single, ValueDistribution.logCounting_coe, ValueDistribution.log_counting_zero_sub_logCounting_top, logCounting_even, toClosedBall_eval_within
instFunLike 📖	CompOp	43 math math: Function.FactorizedRational.divisor, AnalyticOnNhd.circleAverage_log_norm, restrict_apply, MeromorphicOn.extract_zeros_poles_log, apply_eq_zero_of_notMem, eq_zero_codiscreteWithin, MeromorphicOn.divisor_sub_const_self, le_def, coe_sub, MeromorphicOn.divisor_sub_const_of_ne, ext_iff, restrict_eqOn_compl, coe_zsmul, single_apply, coe_sum, memAddSubmonoid, MeromorphicOn.divisor_apply, coe_single, restrict_eqOn, mk_of_mem_addSubmonoid_toFun, MeromorphicNFOn.zero_set_eq_divisor_support, MeromorphicOn.circleAverage_log_norm, coe_nsmul, posPart_apply, mk_of_mem_addSubgroup_toFun, circleAverage_log_norm_factorizedRational, MeromorphicOn.min_divisor_le_divisor_add, MeromorphicOn.extract_zeros_poles, AnalyticOnNhd.sum_divisor_le, sum_apply_smul_single_eq_self, coe_add, MeromorphicOn.AnalyticOnNhd.divisor_apply, MeromorphicOn.divisor_def, coe_zero, negPart_apply, coe_injective, coe_finsum, coe_neg, min_apply, max_apply, lt_def, memAddSubgroup, toClosedBall_eval_within
instLE 📖	CompOp	9 math math: posPart_add, le_def, exists_single_le_pos, single_nonneg, MeromorphicNFOn.divisor_nonneg_iff_analyticOnNhd, negPart_add, MeromorphicOn.AnalyticOnNhd.divisor_nonneg, MeromorphicOn.negPart_divisor_add_le_max, MeromorphicOn.negPart_divisor_add_le_add
instLTOfPreorder 📖	CompOp	4 math math: single_pos, single_pos_int_one, single_pos_nat_one, lt_def
instLattice 📖	CompOp	17 math math: ValueDistribution.logCounting_zero, nsmul_posPart, ValueDistribution.logCounting_top, posPart_add, instIsOrderedAddMonoid, MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_right, MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_left, negPart_add, posPart_apply, restrict_posPart, MeromorphicOn.negPart_divisor_add_le_max, nsmul_negPart, MeromorphicOn.negPart_divisor_add_le_add, restrictLatticeHom_apply, restrict_negPart, negPart_apply, ValueDistribution.logCounting_coe
instMaxOfSemilatticeSup 📖	CompOp	2 math math: MeromorphicOn.negPart_divisor_add_le_max, max_apply
instMinOfSemilatticeInf 📖	CompOp	1 math math: min_apply
instNeg 📖	CompOp	3 math math: MeromorphicOn.divisor_inv, MeromorphicOn.divisor_fun_inv, coe_neg
instSMulInt 📖	CompOp	3 math math: coe_zsmul, MeromorphicOn.divisor_fun_zpow, MeromorphicOn.divisor_zpow
instSMulNat 📖	CompOp	5 math math: MeromorphicOn.divisor_pow, nsmul_posPart, MeromorphicOn.divisor_fun_pow, coe_nsmul, nsmul_negPart
instSub 📖	CompOp	1 math math: coe_sub
instZero 📖	CompOp	10 math math: MeromorphicOn.divisor_const, zero_iff_logCounting_bounded, MeromorphicOn.divisor_natCast, MeromorphicOn.divisor_intCast, MeromorphicOn.divisor_ofNat, MeromorphicNFOn.divisor_nonneg_iff_analyticOnNhd, MeromorphicOn.AnalyticOnNhd.divisor_nonneg, coe_zero, single_pos_int_one, single_pos_nat_one
mk_of_mem 📖	CompOp	—
mk_of_mem_addSubgroup 📖	CompOp	1 math math: mk_of_mem_addSubgroup_toFun
mk_of_mem_addSubmonoid 📖	CompOp	1 math math: mk_of_mem_addSubmonoid_toFun
restrict 📖	CompOp	10 math math: restrict_apply, restrict_zero, restrict_eqOn_compl, MeromorphicOn.divisor_restrict, restrict_eqOn, restrict_posPart, restrictMonoidHom_apply, sum_apply_smul_single_eq_self, restrictLatticeHom_apply, restrict_negPart
restrictLatticeHom 📖	CompOp	1 math math: restrictLatticeHom_apply
restrictMonoidHom 📖	CompOp	1 math math: restrictMonoidHom_apply
single 📖	CompOp	11 math math: logCounting_single_eq_log_sub_const, single_zero, single_apply, single_pos, exists_single_le_pos, coe_single, single_nonneg, sum_apply_smul_single_eq_self, one_isLittleO_logCounting_single, single_pos_int_one, single_pos_nat_one
support 📖	CompOp	6 math math: toClosedBall_support_subset_closedBall, supportLocallyFiniteWithinDomain, finiteSupport, discreteSupport, supportWithinDomain, closedSupport
toFun 📖	CompOp	3 math math: supportWithinDomain', Function.locallyFinsupp.locallyFiniteSupport, supportLocallyFiniteWithinDomain'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_zero_of_notMem 📖	mathematical	Set Set.instMembership	DFunLike.coe Function.locallyFinsuppWithin instFunLike	—	Function.notMem_support supportWithinDomain
closedSupport 📖	mathematical	—	IsClosed support	—	Set.ext supportWithinDomain isClosed_sdiff_of_codiscreteWithin supportDiscreteWithin_iff_locallyFiniteWithin supportLocallyFiniteWithinDomain
coe_add 📖	mathematical	—	DFunLike.coe Function.locallyFinsuppWithin AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass instFunLike instAdd Pi.instAdd AddSemigroup.toAdd AddMonoid.toAddSemigroup	—	—
coe_finsum 📖	mathematical	—	DFunLike.coe Function.locallyFinsuppWithin MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing instFunLike finsum instAddCommMonoid Int.instAddCommMonoid Pi.addCommMonoid	—	finsum_eq_sum coe_sum Finset.sum_congr Set.Finite.toFinset.congr_simp finsum_of_infinite_support
coe_injective 📖	mathematical	—	Function.locallyFinsuppWithin DFunLike.coe instFunLike	—	DFunLike.coe_injective
coe_neg 📖	mathematical	—	DFunLike.coe Function.locallyFinsuppWithin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid instFunLike instNeg Pi.instNeg NegZeroClass.toNeg	—	—
coe_nsmul 📖	mathematical	—	DFunLike.coe Function.locallyFinsuppWithin AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass instFunLike instSMulNat AddMonoid.toNSMul Pi.addMonoid	—	—
coe_single 📖	mathematical	—	DFunLike.coe Function.locallyFinsupp instFunLike Set.univ single Pi.single	—	single_apply Pi.single_apply
coe_sub 📖	mathematical	—	DFunLike.coe Function.locallyFinsuppWithin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid instFunLike instSub Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	—
coe_sum 📖	mathematical	—	DFunLike.coe Function.locallyFinsuppWithin AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike Finset.sum instAddCommMonoid Pi.addCommMonoid	—	Finset.induction Finset.sum_insert
coe_zero 📖	mathematical	—	DFunLike.coe Function.locallyFinsuppWithin AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass instFunLike instZero Pi.instZero	—	—
coe_zsmul 📖	mathematical	—	DFunLike.coe Function.locallyFinsuppWithin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid instFunLike instSMulInt SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid	—	—
discreteSupport 📖	mathematical	—	IsDiscrete support	—	Set.ext supportWithinDomain Set.mem_setOf_eq Set.mem_compl_iff Set.mem_inter_iff isDiscrete_of_codiscreteWithin compl_compl supportDiscreteWithin_iff_locallyFiniteWithin supportLocallyFiniteWithinDomain
eq_zero_codiscreteWithin 📖	mathematical	—	Filter.EventuallyEq Filter.codiscreteWithin DFunLike.coe Function.locallyFinsuppWithin instFunLike Pi.instZero	—	codiscreteWithin_iff_locallyFiniteComplementWithin Set.ext Function.support_subset_iff supportWithinDomain supportLocallyFiniteWithinDomain
exists_single_le_pos 📖	mathematical	Function.locallyFinsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing instLTOfPreorder Set.univ PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt instZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	Function.locallyFinsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing instLE Set.univ single	—	ext_iff ne_of_lt eq_or_ne single_apply LT.lt.le
ext 📖	—	DFunLike.coe Function.locallyFinsuppWithin instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe Function.locallyFinsuppWithin instFunLike	—	ext
finiteSupport 📖	mathematical	IsCompact	Set.Finite support	—	IsCompact.finite IsCompact.of_isClosed_subset closedSupport T2Space.t1Space IsCompact.isClosed supportWithinDomain discreteSupport
instIsOrderedAddMonoid 📖	mathematical	—	IsOrderedAddMonoid Function.locallyFinsuppWithin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommMonoid AddCommGroup.toAddCommMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLattice DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Pi.isOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT Pi.instIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedCancelAddMonoid.toAddLeftReflectLT Pi.isOrderedAddCancelMonoid
le_def 📖	mathematical	—	Function.locallyFinsuppWithin instLE Pi.hasLe DFunLike.coe instFunLike	—	—
lt_def 📖	mathematical	—	Function.locallyFinsuppWithin instLTOfPreorder Preorder.toLT Pi.preorder DFunLike.coe instFunLike	—	—
max_apply 📖	mathematical	—	DFunLike.coe Function.locallyFinsuppWithin instFunLike instMaxOfSemilatticeSup SemilatticeSup.toMax	—	—
memAddSubgroup 📖	mathematical	—	AddSubgroup Pi.addGroup SetLike.instMembership AddSubgroup.instSetLike addSubgroup DFunLike.coe Function.locallyFinsuppWithin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid instFunLike	—	supportWithinDomain supportLocallyFiniteWithinDomain
memAddSubmonoid 📖	mathematical	—	AddSubmonoid Pi.addZeroClass AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike addSubmonoid DFunLike.coe Function.locallyFinsuppWithin AddZero.toZero AddZeroClass.toAddZero instFunLike	—	supportWithinDomain supportLocallyFiniteWithinDomain
min_apply 📖	mathematical	—	DFunLike.coe Function.locallyFinsuppWithin instFunLike instMinOfSemilatticeInf SemilatticeInf.toMin	—	—
mk_of_mem_addSubgroup_toFun 📖	mathematical	AddSubgroup Pi.addGroup SetLike.instMembership AddSubgroup.instSetLike addSubgroup	DFunLike.coe Function.locallyFinsuppWithin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid instFunLike mk_of_mem_addSubgroup	—	—
mk_of_mem_addSubmonoid_toFun 📖	mathematical	AddSubmonoid Pi.addZeroClass AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike addSubmonoid	DFunLike.coe Function.locallyFinsuppWithin AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass instFunLike mk_of_mem_addSubmonoid	—	—
negPart_add 📖	mathematical	—	Function.locallyFinsuppWithin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instLE Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegPart.negPart instNegPart instLattice instAddGroup AddCommGroup.toAddGroup instAdd SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid	—	negPart_def neg_add_rev add_comm IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add
negPart_apply 📖	mathematical	—	DFunLike.coe Function.locallyFinsuppWithin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instFunLike NegPart.negPart instNegPart instLattice instAddGroup AddCommGroup.toAddGroup	—	—
nsmul_negPart 📖	mathematical	—	NegPart.negPart Function.locallyFinsuppWithin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instNegPart instLattice DistribLattice.toLattice instDistribLatticeOfLinearOrder instAddGroup AddCommGroup.toAddGroup instSMulNat SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid	—	ext max_eq_right_of_lt nsmul_zero IsOrderedAddMonoid.toAddLeftMono smul_neg nsmul_le_nsmul_right covariant_swap_add_of_covariant_add LT.lt.le sup_of_le_left not_lt nsmul_nonneg
nsmul_posPart 📖	mathematical	—	PosPart.posPart Function.locallyFinsuppWithin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instPosPart instLattice DistribLattice.toLattice instDistribLatticeOfLinearOrder instAddGroup AddCommGroup.toAddGroup instSMulNat SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid	—	ext max_eq_right_of_lt nsmul_zero nsmul_le_nsmul_right IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add LT.lt.le sup_of_le_left not_lt nsmul_nonneg
posPart_add 📖	mathematical	—	Function.locallyFinsuppWithin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instLE Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder PosPart.posPart instPosPart instLattice instAddGroup AddCommGroup.toAddGroup instAdd SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid	—	posPart_def IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add
posPart_apply 📖	mathematical	—	DFunLike.coe Function.locallyFinsuppWithin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instFunLike PosPart.posPart instPosPart instLattice instAddGroup AddCommGroup.toAddGroup	—	—
restrictLatticeHom_apply 📖	mathematical	Set Set.instHasSubset	DFunLike.coe LatticeHom Function.locallyFinsuppWithin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instLattice LatticeHom.instFunLike restrictLatticeHom restrict	—	—
restrictMonoidHom_apply 📖	mathematical	Set Set.instHasSubset	DFunLike.coe AddMonoidHom Function.locallyFinsuppWithin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid AddMonoidHom.instFunLike restrictMonoidHom restrict	—	—
restrict_apply 📖	mathematical	Set Set.instHasSubset	DFunLike.coe Function.locallyFinsuppWithin instFunLike restrict Set Set.instMembership	—	—
restrict_eqOn 📖	mathematical	Set Set.instHasSubset	Set.EqOn DFunLike.coe Function.locallyFinsuppWithin instFunLike restrict	—	—
restrict_eqOn_compl 📖	mathematical	Set Set.instHasSubset	Set.EqOn DFunLike.coe Function.locallyFinsuppWithin instFunLike restrict Pi.instZero Compl.compl Set Set.instCompl	—	apply_eq_zero_of_notMem
restrict_negPart 📖	mathematical	Set Set.instHasSubset	restrict MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing NegPart.negPart Function.locallyFinsuppWithin instNegPart instLattice instLatticeInt instAddGroup Int.instAddGroup	—	ext negPart_of_nonpos Int.instAddLeftMono instReflLe neg_zero
restrict_posPart 📖	mathematical	Set Set.instHasSubset	restrict MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing PosPart.posPart Function.locallyFinsuppWithin instPosPart instLattice instLatticeInt instAddGroup Int.instAddGroup	—	ext posPart_zero
restrict_zero 📖	mathematical	Set Set.instHasSubset	restrict Function.locallyFinsuppWithin instZeroLocallyFinsuppWithin	—	ext restrict_apply apply_eq_zero_of_notMem
single_apply 📖	mathematical	—	DFunLike.coe Function.locallyFinsupp instFunLike Set.univ single	—	Pi.single_apply
single_nonneg 📖	mathematical	—	Function.locallyFinsupp instLE Set.univ Preorder.toLE instZeroLocallyFinsuppWithin single	—	coe_single Pi.single_nonneg
single_pos 📖	mathematical	—	Function.locallyFinsupp instLTOfPreorder Set.univ instZeroLocallyFinsuppWithin single Preorder.toLT	—	lt_def coe_single Pi.single_pos
single_pos_int_one 📖	mathematical	—	Function.locallyFinsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing instLTOfPreorder Set.univ PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt instZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid single	—	single_pos
single_pos_nat_one 📖	mathematical	—	Function.locallyFinsupp MulZeroClass.toZero Nat.instMulZeroClass instLTOfPreorder Set.univ Nat.instPreorder instZero Nat.instAddMonoid single	—	single_pos
single_zero 📖	mathematical	—	single Function.locallyFinsupp instZeroLocallyFinsuppWithin Set.univ	—	ext single_apply
sum_apply_smul_single_eq_self 📖	mathematical	—	finsum Function.locallyFinsuppWithin AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid restrict Set.univ single DFunLike.coe instFunLike Set.subset_univ	—	Set.subset_univ Mathlib.Tactic.Contrapose.contrapose₁ restrict.congr_simp Set.Finite.coe_toFinset single_zero restrict_zero finsum_eq_sum_of_support_subset ext apply_eq_zero_of_notMem coe_sum Finset.sum_apply Finset.sum_congr single_apply Finset.sum_ite_irrel Finset.sum_ite_eq Finset.sum_const_zero
supportLocallyFiniteWithinDomain 📖	mathematical	Set Set.instMembership	Set Filter Filter.instMembership nhds Set.Finite Set.instInter support	—	supportLocallyFiniteWithinDomain'
supportLocallyFiniteWithinDomain' 📖	mathematical	Set Set.instMembership	Set Filter Filter.instMembership nhds Set.Finite Set.instInter Function.support toFun	—	—
supportWithinDomain 📖	mathematical	—	Set Set.instHasSubset support	—	supportWithinDomain'
supportWithinDomain' 📖	mathematical	—	Set Set.instHasSubset Function.support toFun	—	—

LocallyFiniteSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_inter_support_of_isCompact 📖	mathematical	LocallyFiniteSupport IsCompact	Set.Finite Set Set.instInter Function.support	—	LocallyFinite.finite_nonempty_inter_compact locallyFinite_support Set.ext Set.Finite.image
iff_locallyFinite_support 📖	mathematical	—	LocallyFinite Set.Elem Function.support Set Set.instSingletonSet Set.instMembership LocallyFiniteSupport	—	Set.ext Set.finite_image_iff
locallyFinite_support 📖	mathematical	LocallyFiniteSupport	LocallyFinite Set.Elem Function.support Set Set.instSingletonSet Set.instMembership	—	iff_locallyFinite_support

(root)

Definitions

Name	Category	Theorems
LocallyFiniteSupport 📖	MathDef	2 math math: LocallyFiniteSupport.iff_locallyFinite_support, Function.locallyFinsupp.locallyFiniteSupport
instZeroLocallyFinsuppWithin 📖	CompOp	4 math math: Function.locallyFinsuppWithin.single_zero, Function.locallyFinsuppWithin.restrict_zero, Function.locallyFinsuppWithin.single_pos, Function.locallyFinsuppWithin.single_nonneg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
supportDiscreteWithin_iff_locallyFiniteWithin 📖	mathematical	Set Set.instHasSubset Function.support	Filter.EventuallyEq Filter.codiscreteWithin Pi.instZero Set Filter Filter.instMembership nhds Set.Finite Set.instInter Function.support	—	Set.ext Filter.EventuallyEq.eq_1 Filter.Eventually.eq_1 codiscreteWithin_iff_locallyFiniteComplementWithin

---

← Back to Index