Basic

📁 Source: Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean

Statistics

Metric	Count
Definitions `RestrictedProduct`, `coeAddMonoidHom`, `coeMonoidHom`, `evalAddMonoidHom`, `evalMonoidHom`, `evalRingHom`, `inclusion`, `instAddCoeOfAddMemClass`, `instAddCommGroupCoeOfAddSubgroupClass`, `instAddCommMonoidCoeOfAddSubmonoidClass`, `instAddGroupCoeOfAddSubgroupClass`, `instAddMonoidCoeOfAddSubmonoidClass`, `instCommGroupCoeOfSubgroupClass`, `instCommMonoidCoeOfSubmonoidClass`, `instCommRingCoeOfSubringClass`, `instDFunLike`, `instDivCoeOfSubgroupClass`, `instGroupCoeOfSubgroupClass`, `instIntCastCoeOfSubringClass`, `instInvCoeOfInvMemClass`, `instModuleCoeOfSMulMemClass`, `instMonoidCoeOfSubmonoidClass`, `instMulCoeOfMulMemClass`, `instNSMul`, `instNatCastCoeOfAddSubmonoidWithOneClass`, `instNegCoeOfNegMemClass`, `instOneCoeOfOneMemClass`, `instPowCoeIntOfSubgroupClass`, `instPowCoeNatOfSubmonoidClass`, `instRingCoeOfSubringClass`, `instSMulCoeOfSMulMemClass`, `instSubCoeOfAddSubgroupClass`, `instVAddCoeOfVAddMemClass`, `instZSMul`, `instZeroCoeOfZeroMemClass`, `map`, `mapAlong`, `mapAlongAddMonoidHom`, `mapAlongMonoidHom`, `mapAlongRingHom`, `mk`, `mulSingle`, `single`, `structureMap`, `«termΠʳ_,[_,_]_[_]»`, `«termΠʳ_,[_,_]»`	46
Theorems `add_apply`, `coe_comp_inclusion`, `coe_comp_structureMap`, `coe_mulSingle_apply`, `coe_single_apply`, `comp_mulSingle`, `comp_single`, `div_apply`, `evalMonoidHom_apply`, `evalRingHom_apply`, `eventually`, `exists_inclusion_eq_of_eventually`, `exists_structureMap_eq_of_forall`, `ext`, `ext_iff`, `image_coe_preimage_inclusion_subset`, `inclusion_apply`, `inclusion_eq_id`, `inv_apply`, `mapAlongAddMonoidHom_apply`, `mapAlongMonoidHom_apply`, `mapAlongRingHom_apply`, `mapAlong_apply`, `map_apply`, `mk_apply`, `mulSingle_div`, `mulSingle_eq_of_ne`, `mulSingle_eq_of_ne'`, `mulSingle_eq_one_iff`, `mulSingle_inj`, `mulSingle_injective`, `mulSingle_inv`, `mulSingle_mul`, `mulSingle_ne_one_iff`, `mulSingle_one`, `mulSingle_pow`, `mulSingle_zpow`, `mul_apply`, `mul_single`, `neg_apply`, `nsmul_apply`, `one_apply`, `pow_apply`, `range_coe`, `range_coe_principal`, `range_inclusion`, `range_structureMap`, `single_add`, `single_eq_of_ne`, `single_eq_of_ne'`, `single_eq_zero_iff`, `single_inj`, `single_injective`, `single_mul`, `single_ne_zero_iff`, `single_neg`, `single_nsmul`, `single_sub`, `single_zero`, `single_zsmul`, `smul_apply`, `structureMap_apply`, `sub_apply`, `vadd_apply`, `zero_apply`, `zpow_apply`, `zsmul_apply`	67
Total	113

RestrictedProduct

Definitions

Name	Category	Theorems
`coeAddMonoidHom` 📖	CompOp	—
`coeMonoidHom` 📖	CompOp	—
`evalAddMonoidHom` 📖	CompOp	—
`evalMonoidHom` 📖	CompOp	1 math math: `evalMonoidHom_apply`
`evalRingHom` 📖	CompOp	1 math math: `evalRingHom_apply`
`inclusion` 📖	CompOp	18 math math: `image_coe_preimage_inclusion_subset`, `inclusion_apply`, `nhds_zero_eq_map_ofPre`, `continuous_dom`, `continuous_dom_prod`, `inclusion_eq_id`, `exists_inclusion_eq_of_eventually`, `continuous_inclusion`, `isEmbedding_inclusion_top`, `continuous_dom_pi`, `range_inclusion`, `continuous_dom_prod_right`, `coe_comp_inclusion`, `isEmbedding_inclusion_principal`, `topologicalSpace_eq_iSup`, `continuous_dom_prod_left`, `isOpenEmbedding_inclusion_principal`, `nhds_eq_map_inclusion`
`instAddCoeOfAddMemClass` 📖	CompOp	4 math math: `instContinuousAddCoePrincipal`, `single_add`, `instContinuousAddCoeCofinite`, `add_apply`
`instAddCommGroupCoeOfAddSubgroupClass` 📖	CompOp	—
`instAddCommMonoidCoeOfAddSubmonoidClass` 📖	CompOp	—
`instAddGroupCoeOfAddSubgroupClass` 📖	CompOp	2 math math: `instIsTopologicalAddGroupCoePrincipal`, `isTopologicalAddGroup`
`instAddMonoidCoeOfAddSubmonoidClass` 📖	CompOp	1 math math: `mapAlongAddMonoidHom_apply`
`instCommGroupCoeOfSubgroupClass` 📖	CompOp	—
`instCommMonoidCoeOfSubmonoidClass` 📖	CompOp	—
`instCommRingCoeOfSubringClass` 📖	CompOp	—
`instDFunLike` 📖	CompOp	54 math math: `image_coe_preimage_inclusion_subset`, `continuous_rng_of_principal`, `one_apply`, `continuous_coe`, `sub_apply`, `single_mul`, `inclusion_apply`, `coe_comp_structureMap`, `mapAlong_apply`, `zsmul_apply`, `mul_single`, `smul_apply`, `nsmul_apply`, `mulSingle_eq_of_ne'`, `continuous_rng_of_top`, `ext_iff`, `coe_single_apply`, `comp_single`, `isEmbedding_coe_of_principal`, `evalRingHom_apply`, `mapAlongRingHom_apply`, `topologicalSpace_eq_of_principal`, `vadd_apply`, `inv_apply`, `range_coe_principal`, `continuous_rng_of_principal_iff_forall`, `range_coe`, `eventually`, `structureMap_apply`, `comp_mulSingle`, `coe_mulSingle_apply`, `single_eq_of_ne`, `zero_apply`, `range_inclusion`, `neg_apply`, `isEmbedding_coe_of_top`, `coe_comp_inclusion`, `continuous_eval`, `topologicalSpace_eq_of_bot`, `mapAlongAddMonoidHom_apply`, `evalMonoidHom_apply`, `mk_apply`, `isEmbedding_coe_of_bot`, `zpow_apply`, `add_apply`, `topologicalSpace_eq_of_top`, `div_apply`, `map_apply`, `mapAlongMonoidHom_apply`, `single_eq_of_ne'`, `continuous_rng_of_bot`, `mulSingle_eq_of_ne`, `pow_apply`, `mul_apply`
`instDivCoeOfSubgroupClass` 📖	CompOp	2 math math: `div_apply`, `mulSingle_div`
`instGroupCoeOfSubgroupClass` 📖	CompOp	2 math math: `instIsTopologicalGroupCoePrincipal`, `isTopologicalGroup`
`instIntCastCoeOfSubringClass` 📖	CompOp	—
`instInvCoeOfInvMemClass` 📖	CompOp	3 math math: `mulSingle_inv`, `inv_apply`, `instContinuousInvCoe`
`instModuleCoeOfSMulMemClass` 📖	CompOp	—
`instMonoidCoeOfSubmonoidClass` 📖	CompOp	2 math math: `evalMonoidHom_apply`, `mapAlongMonoidHom_apply`
`instMulCoeOfMulMemClass` 📖	CompOp	6 math math: `instContinuousMulCoePrincipal`, `single_mul`, `mul_single`, `mulSingle_mul`, `instContinuousMulCoeCofinite`, `mul_apply`
`instNSMul` 📖	CompOp	2 math math: `nsmul_apply`, `single_nsmul`
`instNatCastCoeOfAddSubmonoidWithOneClass` 📖	CompOp	—
`instNegCoeOfNegMemClass` 📖	CompOp	3 math math: `instContinuousNegCoe`, `neg_apply`, `single_neg`
`instOneCoeOfOneMemClass` 📖	CompOp	3 math math: `one_apply`, `mulSingle_one`, `mulSingle_eq_one_iff`
`instPowCoeIntOfSubgroupClass` 📖	CompOp	2 math math: `mulSingle_zpow`, `zpow_apply`
`instPowCoeNatOfSubmonoidClass` 📖	CompOp	2 math math: `mulSingle_pow`, `pow_apply`
`instRingCoeOfSubringClass` 📖	CompOp	4 math math: `instIsTopologicalRingCoePrincipal`, `evalRingHom_apply`, `mapAlongRingHom_apply`, `isTopologicalRing`
`instSMulCoeOfSMulMemClass` 📖	CompOp	4 math math: `smul_apply`, `instContinuousConstSMulCoe`, `instContinuousSMulCoePrincipal`, `continuousSMul`
`instSubCoeOfAddSubgroupClass` 📖	CompOp	2 math math: `sub_apply`, `single_sub`
`instVAddCoeOfVAddMemClass` 📖	CompOp	4 math math: `vadd_apply`, `instContinuousConstVAddCoe`, `continuousVAdd`, `instContinuousVAddCoePrincipal`
`instZSMul` 📖	CompOp	2 math math: `zsmul_apply`, `single_zsmul`
`instZeroCoeOfZeroMemClass` 📖	CompOp	4 math math: `single_eq_zero_iff`, `nhds_zero_eq_map_ofPre`, `single_zero`, `zero_apply`
`map` 📖	CompOp	1 math math: `map_apply`
`mapAlong` 📖	CompOp	2 math math: `mapAlong_apply`, `mapAlong_continuous`
`mapAlongAddMonoidHom` 📖	CompOp	1 math math: `mapAlongAddMonoidHom_apply`
`mapAlongMonoidHom` 📖	CompOp	1 math math: `mapAlongMonoidHom_apply`
`mapAlongRingHom` 📖	CompOp	1 math math: `mapAlongRingHom_apply`
`mk` 📖	CompOp	—
`mulSingle` 📖	CompOp	13 math math: `mulSingle_inv`, `mulSingle_zpow`, `mulSingle_injective`, `mulSingle_eq_of_ne'`, `mulSingle_mul`, `comp_mulSingle`, `coe_mulSingle_apply`, `mulSingle_one`, `mulSingle_pow`, `mulSingle_inj`, `mulSingle_div`, `mulSingle_eq_of_ne`, `mulSingle_eq_one_iff`
`single` 📖	CompOp	15 math math: `single_injective`, `single_eq_zero_iff`, `single_mul`, `mul_single`, `coe_single_apply`, `single_zero`, `comp_single`, `single_add`, `single_sub`, `single_inj`, `single_eq_of_ne`, `single_nsmul`, `single_zsmul`, `single_neg`, `single_eq_of_ne'`
`structureMap` 📖	CompOp	8 math math: `coe_comp_structureMap`, `isOpenEmbedding_structureMap`, `nhds_eq_map_structureMap`, `structureMap_apply`, `exists_structureMap_eq_of_forall`, `nhds_zero_eq_map_structureMap`, `isEmbedding_structureMap`, `range_structureMap`
`«termΠʳ_,[_,_]_[_]»` 📖	CompOp	—
`«termΠʳ_,[_,_]»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	`AddMemClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `instDFunLike` `instAddCoeOfAddMemClass`	—	—
`coe_comp_inclusion` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	`RestrictedProduct` `DFunLike.coe` `instDFunLike` `inclusion`	—	—
`coe_comp_structureMap` 📖	mathematical	—	`RestrictedProduct` `DFunLike.coe` `instDFunLike` `structureMap` `Set` `Set.instMembership`	—	—
`coe_mulSingle_apply` 📖	mathematical	`OneMemClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instDFunLike` `mulSingle` `Pi.mulSingle`	—	—
`coe_single_apply` 📖	mathematical	`ZeroMemClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instDFunLike` `single` `Pi.single`	—	—
`comp_mulSingle` 📖	mathematical	`OneMemClass`	`RestrictedProduct` `SetLike.coe` `Filter.cofinite` `DFunLike.coe` `instDFunLike` `mulSingle` `Pi.mulSingle`	—	—
`comp_single` 📖	mathematical	`ZeroMemClass`	`RestrictedProduct` `SetLike.coe` `Filter.cofinite` `DFunLike.coe` `instDFunLike` `single` `Pi.single`	—	—
`div_apply` 📖	mathematical	`SubgroupClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `instDFunLike` `instDivCoeOfSubgroupClass` `DivInvMonoid.toDiv`	—	—
`evalMonoidHom_apply` 📖	mathematical	`SubmonoidClass` `Monoid.toMulOneClass`	`DFunLike.coe` `MonoidHom` `RestrictedProduct` `SetLike.coe` `MulOneClass.toMulOne` `instMonoidCoeOfSubmonoidClass` `MonoidHom.instFunLike` `evalMonoidHom` `instDFunLike`	—	—
`evalRingHom_apply` 📖	mathematical	`SubringClass`	`DFunLike.coe` `RingHom` `RestrictedProduct` `SetLike.coe` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instRingCoeOfSubringClass` `RingHom.instFunLike` `evalRingHom` `instDFunLike`	—	—
`eventually` 📖	mathematical	—	`Filter.Eventually` `Set` `Set.instMembership` `DFunLike.coe` `RestrictedProduct` `instDFunLike`	—	—
`exists_inclusion_eq_of_eventually` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.Eventually` `Set` `Set.instMembership` `DFunLike.coe` `RestrictedProduct` `instDFunLike`	`inclusion`	—	—
`exists_structureMap_eq_of_forall` 📖	mathematical	`Set` `Set.instMembership` `Filter.Eventually`	`structureMap`	—	—
`ext` 📖	—	`DFunLike.coe` `RestrictedProduct` `instDFunLike`	—	—	—
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `RestrictedProduct` `instDFunLike`	—	`ext`
`image_coe_preimage_inclusion_subset` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	`Set` `Set.instHasSubset` `Set.image` `RestrictedProduct` `DFunLike.coe` `instDFunLike` `Set.preimage` `inclusion`	—	—
`inclusion_apply` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	`DFunLike.coe` `RestrictedProduct` `instDFunLike` `inclusion`	—	—
`inclusion_eq_id` 📖	mathematical	—	`inclusion` `le_refl` `Filter` `PartialOrder.toPreorder` `Filter.instPartialOrder` `RestrictedProduct`	—	`le_refl`
`inv_apply` 📖	mathematical	`InvMemClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `instDFunLike` `instInvCoeOfInvMemClass`	—	—
`mapAlongAddMonoidHom_apply` 📖	mathematical	`Filter.Tendsto` `AddSubmonoidClass` `AddMonoid.toAddZeroClass` `Filter.Eventually` `Set.MapsTo` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `SetLike.coe`	`RestrictedProduct` `instDFunLike` `instAddMonoidCoeOfAddSubmonoidClass` `mapAlongAddMonoidHom`	—	—
`mapAlongMonoidHom_apply` 📖	mathematical	`Filter.Tendsto` `SubmonoidClass` `Monoid.toMulOneClass` `Filter.Eventually` `Set.MapsTo` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MonoidHom.instFunLike` `SetLike.coe`	`RestrictedProduct` `instDFunLike` `instMonoidCoeOfSubmonoidClass` `mapAlongMonoidHom`	—	—
`mapAlongRingHom_apply` 📖	mathematical	`Filter.Tendsto` `SubringClass` `Filter.Eventually` `Set.MapsTo` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike` `SetLike.coe`	`RestrictedProduct` `instDFunLike` `instRingCoeOfSubringClass` `mapAlongRingHom`	—	—
`mapAlong_apply` 📖	mathematical	`Filter.Tendsto` `Filter.Eventually` `Set.MapsTo`	`DFunLike.coe` `RestrictedProduct` `instDFunLike` `mapAlong`	—	—
`map_apply` 📖	mathematical	`Filter.Eventually` `Set.MapsTo`	`DFunLike.coe` `RestrictedProduct` `instDFunLike` `map`	—	—
`mk_apply` 📖	mathematical	`Filter.Eventually` `Set` `Set.instMembership`	`DFunLike.coe` `RestrictedProduct` `instDFunLike`	—	—
`mulSingle_div` 📖	mathematical	`SubgroupClass` `Group.toDivInvMonoid`	`mulSingle` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SubmonoidClass.toOneMemClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `SubgroupClass.toSubmonoidClass` `DivInvMonoid.toDiv` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instDivCoeOfSubgroupClass`	—	`ext` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `Pi.mulSingle_div`
`mulSingle_eq_of_ne` 📖	mathematical	`OneMemClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instDFunLike` `mulSingle`	—	`Pi.mulSingle_eq_of_ne`
`mulSingle_eq_of_ne'` 📖	mathematical	`OneMemClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instDFunLike` `mulSingle`	—	`Pi.mulSingle_eq_of_ne'`
`mulSingle_eq_one_iff` 📖	mathematical	`OneMemClass`	`mulSingle` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instOneCoeOfOneMemClass`	—	`Pi.mulSingle_eq_one_iff`
`mulSingle_inj` 📖	mathematical	`OneMemClass`	`mulSingle`	—	`mulSingle_injective`
`mulSingle_injective` 📖	mathematical	`OneMemClass`	`RestrictedProduct` `SetLike.coe` `Filter.cofinite` `mulSingle`	—	`Function.Injective.of_comp` `Pi.mulSingle_injective` `comp_mulSingle`
`mulSingle_inv` 📖	mathematical	`SubgroupClass` `Group.toDivInvMonoid`	`mulSingle` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SubmonoidClass.toOneMemClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `SubgroupClass.toSubmonoidClass` `InvOneClass.toInv` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instInvCoeOfInvMemClass` `SubgroupClass.toInvMemClass`	—	`ext` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `SubgroupClass.toInvMemClass` `Pi.mulSingle_inv`
`mulSingle_mul` 📖	mathematical	`OneMemClass` `MulOne.toOne` `MulOneClass.toMulOne` `MulMemClass` `MulOne.toMul`	`mulSingle` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instMulCoeOfMulMemClass`	—	`ext` `Pi.mulSingle_mul`
`mulSingle_ne_one_iff` 📖	—	`OneMemClass`	—	—	`Subtype.coe_ne_coe` `Pi.mulSingle_ne_one_iff`
`mulSingle_one` 📖	mathematical	`OneMemClass`	`mulSingle` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instOneCoeOfOneMemClass`	—	`ext` `Pi.mulSingle_one`
`mulSingle_pow` 📖	mathematical	`SubmonoidClass` `Monoid.toMulOneClass`	`mulSingle` `MulOne.toOne` `MulOneClass.toMulOne` `SubmonoidClass.toOneMemClass` `Monoid.toNatPow` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instPowCoeNatOfSubmonoidClass`	—	`ext` `SubmonoidClass.toOneMemClass` `Pi.mulSingle_pow`
`mulSingle_zpow` 📖	mathematical	`SubgroupClass` `Group.toDivInvMonoid`	`mulSingle` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SubmonoidClass.toOneMemClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `SubgroupClass.toSubmonoidClass` `DivInvMonoid.toZPow` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instPowCoeIntOfSubgroupClass`	—	`ext` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `Pi.mulSingle_zpow`
`mul_apply` 📖	mathematical	`MulMemClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `instDFunLike` `instMulCoeOfMulMemClass`	—	—
`mul_single` 📖	mathematical	`ZeroMemClass` `MulZeroClass.toZero` `MulMemClass` `MulZeroClass.toMul`	`single` `DFunLike.coe` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instDFunLike` `instMulCoeOfMulMemClass`	—	`ext` `eq_or_ne` `Pi.single_eq_same` `single_eq_of_ne'` `MulZeroClass.mul_zero`
`neg_apply` 📖	mathematical	`NegMemClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `instDFunLike` `instNegCoeOfNegMemClass`	—	—
`nsmul_apply` 📖	mathematical	`AddSubmonoidClass` `AddMonoid.toAddZeroClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `instDFunLike` `instNSMul` `AddMonoid.toNatSMul`	—	—
`one_apply` 📖	mathematical	`OneMemClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `instDFunLike` `instOneCoeOfOneMemClass`	—	—
`pow_apply` 📖	mathematical	`SubmonoidClass` `Monoid.toMulOneClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `instDFunLike` `instPowCoeNatOfSubmonoidClass` `Monoid.toNatPow`	—	—
`range_coe` 📖	mathematical	—	`Set.range` `RestrictedProduct` `DFunLike.coe` `instDFunLike` `setOf` `Filter.Eventually` `Set` `Set.instMembership`	—	`Subtype.range_val_subtype`
`range_coe_principal` 📖	mathematical	—	`Set.range` `RestrictedProduct` `Filter.principal` `DFunLike.coe` `instDFunLike` `Set.pi`	—	`range_coe`
`range_inclusion` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	`Set.range` `RestrictedProduct` `inclusion` `setOf` `Filter.Eventually` `Set` `Set.instMembership` `DFunLike.coe` `instDFunLike`	—	`subset_antisymm` `Set.instAntisymmSubset` `Set.range_subset_iff` `Set.mem_range` `exists_inclusion_eq_of_eventually`
`range_structureMap` 📖	mathematical	—	`Set.range` `RestrictedProduct` `structureMap` `setOf`	—	`subset_antisymm` `Set.instAntisymmSubset` `Set.range_subset_iff` `Set.mem_range` `exists_structureMap_eq_of_forall`
`single_add` 📖	mathematical	`ZeroMemClass` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMemClass` `AddZero.toAdd`	`single` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instAddCoeOfAddMemClass`	—	`ext` `Pi.single_add`
`single_eq_of_ne` 📖	mathematical	`ZeroMemClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instDFunLike` `single`	—	`Pi.single_eq_of_ne`
`single_eq_of_ne'` 📖	mathematical	`ZeroMemClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instDFunLike` `single`	—	`Pi.single_eq_of_ne'`
`single_eq_zero_iff` 📖	mathematical	`ZeroMemClass`	`single` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instZeroCoeOfZeroMemClass`	—	`Pi.single_eq_zero_iff`
`single_inj` 📖	mathematical	`ZeroMemClass`	`single`	—	`single_injective`
`single_injective` 📖	mathematical	`ZeroMemClass`	`RestrictedProduct` `SetLike.coe` `Filter.cofinite` `single`	—	`Function.Injective.of_comp` `Pi.single_injective` `comp_single`
`single_mul` 📖	mathematical	`ZeroMemClass` `MulZeroClass.toZero` `MulMemClass` `MulZeroClass.toMul`	`single` `DFunLike.coe` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instDFunLike` `instMulCoeOfMulMemClass`	—	`ext` `eq_or_ne` `Pi.single_eq_same` `single_eq_of_ne'` `MulZeroClass.zero_mul`
`single_ne_zero_iff` 📖	—	`ZeroMemClass`	—	—	`Subtype.coe_ne_coe` `Pi.single_ne_zero_iff`
`single_neg` 📖	mathematical	`AddSubgroupClass` `AddGroup.toSubNegMonoid`	`single` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddSubgroupClass.toAddSubmonoidClass` `NegZeroClass.toNeg` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instNegCoeOfNegMemClass` `AddSubgroupClass.toNegMemClass`	—	`ext` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `AddSubgroupClass.toNegMemClass` `Pi.single_neg`
`single_nsmul` 📖	mathematical	`AddSubmonoidClass` `AddMonoid.toAddZeroClass`	`single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toNatSMul` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instNSMul`	—	`ext` `AddSubmonoidClass.toZeroMemClass` `Pi.single_nsmul`
`single_sub` 📖	mathematical	`AddSubgroupClass` `AddGroup.toSubNegMonoid`	`single` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddSubgroupClass.toAddSubmonoidClass` `SubNegMonoid.toSub` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instSubCoeOfAddSubgroupClass`	—	`ext` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `Pi.single_sub`
`single_zero` 📖	mathematical	`ZeroMemClass`	`single` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instZeroCoeOfZeroMemClass`	—	`ext` `Pi.single_zero`
`single_zsmul` 📖	mathematical	`AddSubgroupClass` `AddGroup.toSubNegMonoid`	`single` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddSubgroupClass.toAddSubmonoidClass` `SubNegMonoid.toZSMul` `RestrictedProduct` `SetLike.coe` `Filter.cofinite` `instZSMul`	—	`ext` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `Pi.single_zsmul`
`smul_apply` 📖	mathematical	`SMulMemClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `instDFunLike` `instSMulCoeOfSMulMemClass`	—	—
`structureMap_apply` 📖	mathematical	—	`DFunLike.coe` `RestrictedProduct` `instDFunLike` `structureMap` `Set` `Set.instMembership`	—	—
`sub_apply` 📖	mathematical	`AddSubgroupClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `instDFunLike` `instSubCoeOfAddSubgroupClass` `SubNegMonoid.toSub`	—	—
`vadd_apply` 📖	mathematical	`VAddMemClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `instDFunLike` `HVAdd.hVAdd` `instHVAdd` `instVAddCoeOfVAddMemClass`	—	—
`zero_apply` 📖	mathematical	`ZeroMemClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `instDFunLike` `instZeroCoeOfZeroMemClass`	—	—
`zpow_apply` 📖	mathematical	`SubgroupClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `instDFunLike` `instPowCoeIntOfSubgroupClass` `DivInvMonoid.toZPow`	—	—
`zsmul_apply` 📖	mathematical	`AddSubgroupClass`	`DFunLike.coe` `RestrictedProduct` `SetLike.coe` `instDFunLike` `instZSMul` `SubNegMonoid.toZSMul`	—	—

(root)

Definitions

Name	Category	Theorems
`RestrictedProduct` 📖	CompOp	122 math math: `RestrictedProduct.single_injective`, `RestrictedProduct.mulSingle_inv`, `RestrictedProduct.image_coe_preimage_inclusion_subset`, `RestrictedProduct.continuous_rng_of_principal`, `RestrictedProduct.instContinuousMulCoePrincipal`, `RestrictedProduct.one_apply`, `RestrictedProduct.continuous_coe`, `RestrictedProduct.mulSingle_zpow`, `RestrictedProduct.single_eq_zero_iff`, `RestrictedProduct.sub_apply`, `RestrictedProduct.single_mul`, `RestrictedProduct.instLocallyCompactSpaceCoeCofiniteOfSubgroupClassOfIsTopologicalGroupOfCompactSpaceSubtypeMem`, `RestrictedProduct.inclusion_apply`, `RestrictedProduct.coe_comp_structureMap`, `RestrictedProduct.nhds_zero_eq_map_ofPre`, `RestrictedProduct.isOpen_forall_mem_of_principal`, `RestrictedProduct.isOpenEmbedding_structureMap`, `RestrictedProduct.mapAlong_apply`, `RestrictedProduct.zsmul_apply`, `RestrictedProduct.instIsTopologicalRingCoePrincipal`, `RestrictedProduct.instContinuousAddCoePrincipal`, `RestrictedProduct.mul_single`, `RestrictedProduct.mulSingle_injective`, `RestrictedProduct.isOpen_forall_imp_mem`, `RestrictedProduct.instWeaklyLocallyCompactSpaceCofiniteOfFactForallIsOpenOfCompactSpaceElem`, `RestrictedProduct.instIsTopologicalAddGroupCoePrincipal`, `RestrictedProduct.smul_apply`, `RestrictedProduct.nsmul_apply`, `RestrictedProduct.continuous_dom`, `RestrictedProduct.continuous_dom_prod`, `RestrictedProduct.isOpen_forall_mem`, `RestrictedProduct.mulSingle_eq_of_ne'`, `RestrictedProduct.continuous_rng_of_top`, `RestrictedProduct.inclusion_eq_id`, `RestrictedProduct.ext_iff`, `RestrictedProduct.instWeaklyLocallyCompactSpacePrincipalOfFactLeFilterCofiniteOfCompactSpaceElem`, `RestrictedProduct.coe_single_apply`, `RestrictedProduct.single_zero`, `RestrictedProduct.locallyCompactSpace_of_group`, `RestrictedProduct.comp_single`, `RestrictedProduct.isEmbedding_coe_of_principal`, `RestrictedProduct.single_add`, `RestrictedProduct.instIsTopologicalGroupCoePrincipal`, `RestrictedProduct.evalRingHom_apply`, `RestrictedProduct.single_sub`, `RestrictedProduct.instContinuousNegCoe`, `RestrictedProduct.mulSingle_mul`, `RestrictedProduct.mapAlongRingHom_apply`, `RestrictedProduct.nhds_eq_map_structureMap`, `RestrictedProduct.topologicalSpace_eq_of_principal`, `RestrictedProduct.weaklyLocallyCompactSpace_of_principal`, `RestrictedProduct.vadd_apply`, `RestrictedProduct.inv_apply`, `RestrictedProduct.isTopologicalRing`, `RestrictedProduct.continuous_inclusion`, `RestrictedProduct.isEmbedding_inclusion_top`, `RestrictedProduct.range_coe_principal`, `RestrictedProduct.instContinuousConstSMulCoe`, `RestrictedProduct.instContinuousMulCoeCofinite`, `RestrictedProduct.continuous_rng_of_principal_iff_forall`, `RestrictedProduct.instContinuousConstVAddCoe`, `RestrictedProduct.range_coe`, `RestrictedProduct.eventually`, `RestrictedProduct.instContinuousSMulCoePrincipal`, `RestrictedProduct.structureMap_apply`, `RestrictedProduct.comp_mulSingle`, `RestrictedProduct.coe_mulSingle_apply`, `RestrictedProduct.continuous_dom_pi`, `RestrictedProduct.single_eq_of_ne`, `RestrictedProduct.mapAlong_continuous`, `RestrictedProduct.mulSingle_one`, `RestrictedProduct.zero_apply`, `RestrictedProduct.range_inclusion`, `RestrictedProduct.instT2Space`, `RestrictedProduct.instLocallyCompactSpaceCoeCofiniteOfAddSubgroupClassOfIsTopologicalAddGroupOfCompactSpaceSubtypeMem`, `RestrictedProduct.single_nsmul`, `RestrictedProduct.continuous_dom_prod_right`, `RestrictedProduct.neg_apply`, `RestrictedProduct.instContinuousAddCoeCofinite`, `RestrictedProduct.isEmbedding_coe_of_top`, `RestrictedProduct.instT0Space`, `RestrictedProduct.mulSingle_pow`, `RestrictedProduct.coe_comp_inclusion`, `RestrictedProduct.single_zsmul`, `RestrictedProduct.continuous_eval`, `RestrictedProduct.topologicalSpace_eq_of_bot`, `RestrictedProduct.single_neg`, `RestrictedProduct.continuousSMul`, `RestrictedProduct.mapAlongAddMonoidHom_apply`, `RestrictedProduct.locallyCompactSpace_of_addGroup`, `RestrictedProduct.evalMonoidHom_apply`, `RestrictedProduct.weaklyLocallyCompactSpace_of_cofinite`, `RestrictedProduct.mk_apply`, `RestrictedProduct.isEmbedding_inclusion_principal`, `RestrictedProduct.isEmbedding_coe_of_bot`, `RestrictedProduct.zpow_apply`, `RestrictedProduct.topologicalSpace_eq_iSup`, `RestrictedProduct.nhds_zero_eq_map_structureMap`, `RestrictedProduct.add_apply`, `RestrictedProduct.topologicalSpace_eq_of_top`, `RestrictedProduct.div_apply`, `RestrictedProduct.continuousVAdd`, `RestrictedProduct.isTopologicalGroup`, `RestrictedProduct.instContinuousInvCoe`, `RestrictedProduct.map_apply`, `RestrictedProduct.instContinuousVAddCoePrincipal`, `RestrictedProduct.mapAlongMonoidHom_apply`, `RestrictedProduct.single_eq_of_ne'`, `RestrictedProduct.mulSingle_div`, `RestrictedProduct.continuous_rng_of_bot`, `RestrictedProduct.continuous_dom_prod_left`, `RestrictedProduct.isTopologicalAddGroup`, `RestrictedProduct.mulSingle_eq_of_ne`, `RestrictedProduct.isOpen_forall_imp_mem_of_principal`, `RestrictedProduct.pow_apply`, `RestrictedProduct.mul_apply`, `RestrictedProduct.isOpenEmbedding_inclusion_principal`, `RestrictedProduct.instT1Space`, `RestrictedProduct.nhds_eq_map_inclusion`, `RestrictedProduct.isEmbedding_structureMap`, `RestrictedProduct.range_structureMap`, `RestrictedProduct.mulSingle_eq_one_iff`

---

← Back to Index