LocallyFinsupp

📁 Source: Mathlib/Topology/LocallyFinsupp.lean

Statistics

Metric	Count
Definitions `locallyFinsupp`, `locallyFinsuppWithin`, `addSubgroup`, `instAdd`, `instAddCommGroup`, `instFunLike`, `instLE`, `instLTOfPreorder`, `instLattice`, `instMaxOfSemilatticeSup`, `instMinOfSemilatticeInf`, `instNeg`, `instSMulInt`, `instSMulNat`, `instSub`, `instZero`, `mk_of_mem`, `restrict`, `restrictLatticeHom`, `restrictMonoidHom`, `support`, `toFun`	22
Theorems `apply_eq_zero_of_notMem`, `closedSupport`, `coe_add`, `coe_injective`, `coe_neg`, `coe_nsmul`, `coe_sub`, `coe_zero`, `coe_zsmul`, `discreteSupport`, `eq_zero_codiscreteWithin`, `ext`, `ext_iff`, `finiteSupport`, `instIsOrderedAddMonoid`, `le_def`, `lt_def`, `max_apply`, `memAddSubgroup`, `min_apply`, `mk_of_mem_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`, `supportLocallyFiniteWithinDomain`, `supportLocallyFiniteWithinDomain'`, `supportWithinDomain`, `supportWithinDomain'`, `supportDiscreteWithin_iff_locallyFiniteWithin`	39
Total	61

Function

Definitions

Name	Category	Theorems
`locallyFinsupp` 📖	CompOp	12 math math: `ValueDistribution.logCounting_zero`, `locallyFinsuppWithin.toClosedBall_support_subset_closedBall`, `locallyFinsuppWithin.logCounting_eval_zero`, `ValueDistribution.logCounting_top`, `locallyFinsuppWithin.toClosedBall_divisor`, `ValueDistribution.characteristic_sub_characteristic_inv`, `locallyFinsuppWithin.logCounting_divisor`, `locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const`, `ValueDistribution.logCounting_coe`, `ValueDistribution.log_counting_zero_sub_logCounting_top`, `locallyFinsuppWithin.logCounting_even`, `locallyFinsuppWithin.toClosedBall_eval_within`
`locallyFinsuppWithin` 📖	CompData	66 math math: `ValueDistribution.logCounting_zero`, `FactorizedRational.divisor`, `locallyFinsuppWithin.toClosedBall_support_subset_closedBall`, `MeromorphicOn.divisor_fun_smul`, `MeromorphicOn.divisor_const`, `MeromorphicOn.divisor_pow`, `locallyFinsuppWithin.restrict_apply`, `MeromorphicOn.divisor_natCast`, `locallyFinsuppWithin.nsmul_posPart`, `ValueDistribution.logCounting_top`, `locallyFinsuppWithin.apply_eq_zero_of_notMem`, `MeromorphicOn.divisor_inv`, `MeromorphicOn.divisor_fun_pow`, `locallyFinsuppWithin.posPart_add`, `locallyFinsuppWithin.eq_zero_codiscreteWithin`, `MeromorphicOn.divisor_sub_const_self`, `MeromorphicOn.divisor_intCast`, `locallyFinsuppWithin.instIsOrderedAddMonoid`, `locallyFinsuppWithin.le_def`, `locallyFinsuppWithin.coe_sub`, `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.mk_of_mem_toFun`, `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`, `MeromorphicOn.divisor_fun_inv`, `MeromorphicNFOn.zero_set_eq_divisor_support`, `MeromorphicOn.circleAverage_log_norm`, `locallyFinsuppWithin.coe_nsmul`, `MeromorphicOn.AnalyticOnNhd.divisor_nonneg`, `locallyFinsuppWithin.posPart_apply`, `circleAverage_log_norm_factorizedRational`, `MeromorphicOn.min_divisor_le_divisor_add`, `locallyFinsuppWithin.restrict_posPart`, `MeromorphicOn.extract_zeros_poles`, `MeromorphicOn.negPart_divisor_add_le_max`, `locallyFinsuppWithin.restrictMonoidHom_apply`, `MeromorphicOn.divisor_smul`, `locallyFinsuppWithin.nsmul_negPart`, `locallyFinsuppWithin.coe_add`, `MeromorphicOn.negPart_divisor_add_le_add`, `locallyFinsuppWithin.restrictLatticeHom_apply`, `MeromorphicOn.divisor_def`, `locallyFinsuppWithin.restrict_negPart`, `locallyFinsuppWithin.coe_zero`, `locallyFinsuppWithin.negPart_apply`, `ValueDistribution.logCounting_coe`, `locallyFinsuppWithin.coe_injective`, `locallyFinsuppWithin.coe_neg`, `locallyFinsuppWithin.min_apply`, `MeromorphicOn.divisor_mul`, `locallyFinsuppWithin.max_apply`, `locallyFinsuppWithin.lt_def`, `locallyFinsuppWithin.memAddSubgroup`, `locallyFinsuppWithin.toClosedBall_eval_within`

Function.locallyFinsuppWithin

Definitions

Name	Category	Theorems
`addSubgroup` 📖	CompOp	1 math math: `memAddSubgroup`
`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	31 math math: `ValueDistribution.logCounting_zero`, `toClosedBall_support_subset_closedBall`, `logCounting_nonneg`, `logCounting_eval_zero`, `nsmul_posPart`, `ValueDistribution.logCounting_top`, `logCounting_eventually_le`, `posPart_add`, `instIsOrderedAddMonoid`, `logCounting_eventuallyLE`, `MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_right`, `toClosedBall_divisor`, `MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_left`, `ValueDistribution.characteristic_sub_characteristic_inv`, `locallyFinsuppWithin.logCounting_divisor`, `negPart_add`, `logCounting_divisor_eq_circleAverage_sub_const`, `posPart_apply`, `restrict_posPart`, `MeromorphicOn.negPart_divisor_add_le_max`, `restrictMonoidHom_apply`, `logCounting_mono`, `nsmul_negPart`, `logCounting_le`, `MeromorphicOn.negPart_divisor_add_le_add`, `restrict_negPart`, `negPart_apply`, `ValueDistribution.logCounting_coe`, `ValueDistribution.log_counting_zero_sub_logCounting_top`, `logCounting_even`, `toClosedBall_eval_within`
`instFunLike` 📖	CompOp	32 math math: `Function.FactorizedRational.divisor`, `restrict_apply`, `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`, `mk_of_mem_toFun`, `MeromorphicOn.divisor_apply`, `restrict_eqOn`, `MeromorphicNFOn.zero_set_eq_divisor_support`, `MeromorphicOn.circleAverage_log_norm`, `coe_nsmul`, `posPart_apply`, `circleAverage_log_norm_factorizedRational`, `MeromorphicOn.min_divisor_le_divisor_add`, `MeromorphicOn.extract_zeros_poles`, `coe_add`, `MeromorphicOn.divisor_def`, `coe_zero`, `negPart_apply`, `coe_injective`, `coe_neg`, `min_apply`, `max_apply`, `lt_def`, `memAddSubgroup`, `toClosedBall_eval_within`
`instLE` 📖	CompOp	7 math math: `posPart_add`, `le_def`, `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	1 math math: `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	7 math math: `MeromorphicOn.divisor_const`, `MeromorphicOn.divisor_natCast`, `MeromorphicOn.divisor_intCast`, `MeromorphicOn.divisor_ofNat`, `MeromorphicNFOn.divisor_nonneg_iff_analyticOnNhd`, `MeromorphicOn.AnalyticOnNhd.divisor_nonneg`, `coe_zero`
`mk_of_mem` 📖	CompOp	1 math math: `mk_of_mem_toFun`
`restrict` 📖	CompOp	8 math math: `restrict_apply`, `restrict_eqOn_compl`, `MeromorphicOn.divisor_restrict`, `restrict_eqOn`, `restrict_posPart`, `restrictMonoidHom_apply`, `restrictLatticeHom_apply`, `restrict_negPart`
`restrictLatticeHom` 📖	CompOp	1 math math: `restrictLatticeHom_apply`
`restrictMonoidHom` 📖	CompOp	1 math math: `restrictMonoidHom_apply`
`support` 📖	CompOp	6 math math: `toClosedBall_support_subset_closedBall`, `supportLocallyFiniteWithinDomain`, `finiteSupport`, `discreteSupport`, `supportWithinDomain`, `closedSupport`
`toFun` 📖	CompOp	2 math math: `supportWithinDomain'`, `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` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instFunLike` `instAdd` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	—
`coe_injective` 📖	mathematical	—	`Function.locallyFinsuppWithin` `DFunLike.coe` `instFunLike`	—	`DFunLike.coe_injective`
`coe_neg` 📖	mathematical	—	`DFunLike.coe` `Function.locallyFinsuppWithin` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instFunLike` `instNeg` `Pi.instNeg` `NegZeroClass.toNeg`	—	—
`coe_nsmul` 📖	mathematical	—	`DFunLike.coe` `Function.locallyFinsuppWithin` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instFunLike` `instSMulNat` `AddMonoid.toNatSMul` `Pi.addMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`coe_sub` 📖	mathematical	—	`DFunLike.coe` `Function.locallyFinsuppWithin` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instFunLike` `instSub` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `Function.locallyFinsuppWithin` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instFunLike` `instZero` `Pi.instZero`	—	—
`coe_zsmul` 📖	mathematical	—	`DFunLike.coe` `Function.locallyFinsuppWithin` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instFunLike` `instSMulInt` `SubNegMonoid.toZSMul` `Pi.subNegMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`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`
`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` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLattice` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Pi.isOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `Pi.instIsRightCancelAdd` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `Pi.isOrderedAddCancelMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`
`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` `AddCommGroup.toAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `addSubgroup` `DFunLike.coe` `Function.locallyFinsuppWithin` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instFunLike`	—	`supportWithinDomain` `supportLocallyFiniteWithinDomain`
`min_apply` 📖	mathematical	—	`DFunLike.coe` `Function.locallyFinsuppWithin` `instFunLike` `instMinOfSemilatticeInf` `SemilatticeInf.toMin`	—	—
`mk_of_mem_toFun` 📖	mathematical	`AddSubgroup` `Pi.addGroup` `AddCommGroup.toAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `addSubgroup`	`DFunLike.coe` `Function.locallyFinsuppWithin` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instFunLike` `mk_of_mem`	—	—
`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` `AddCommGroup.toAddGroup` `instAddCommGroup` `instAdd`	—	`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` `AddCommGroup.toAddGroup` `instAddCommGroup`	—	—
`nsmul_negPart` 📖	mathematical	—	`NegPart.negPart` `Function.locallyFinsuppWithin` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instNegPart` `instLattice` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddGroup` `instAddCommGroup` `instSMulNat`	—	`ext` `max_eq_right_of_lt` `nsmul_zero` `IsOrderedAddMonoid.toAddLeftMono` `neg_nsmul` `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` `AddCommGroup.toAddGroup` `instAddCommGroup` `instSMulNat`	—	`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` `AddCommGroup.toAddGroup` `instAddCommGroup` `instAdd`	—	`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` `AddCommGroup.toAddGroup` `instAddCommGroup`	—	—
`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` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `AddMonoidHom.instFunLike` `restrictMonoidHom` `restrict`	—	—
`restrict_apply` 📖	mathematical	`Set` `Set.instHasSubset`	`DFunLike.coe` `Function.locallyFinsuppWithin` `instFunLike` `restrict` `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.instCompl`	—	`apply_eq_zero_of_notMem`
`restrict_negPart` 📖	mathematical	`Set` `Set.instHasSubset`	`restrict` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Int.instAddCommGroup` `NegPart.negPart` `Function.locallyFinsuppWithin` `instNegPart` `instLattice` `instLatticeInt` `AddCommGroup.toAddGroup` `instAddCommGroup`	—	`ext` `negPart_of_nonpos` `Int.instAddLeftMono` `neg_zero`
`restrict_posPart` 📖	mathematical	`Set` `Set.instHasSubset`	`restrict` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Int.instAddCommGroup` `PosPart.posPart` `Function.locallyFinsuppWithin` `instPosPart` `instLattice` `instLatticeInt` `AddCommGroup.toAddGroup` `instAddCommGroup`	—	`ext` `posPart_zero`
`supportLocallyFiniteWithinDomain` 📖	mathematical	`Set` `Set.instMembership`	`Filter` `Filter.instMembership` `nhds` `Set.Finite` `Set.instInter` `support`	—	`supportLocallyFiniteWithinDomain'`
`supportLocallyFiniteWithinDomain'` 📖	mathematical	`Set` `Set.instMembership`	`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`	—	—

(root)

Theorems

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

---

← Back to Index