ContinuousMonoidHom

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

Statistics

Metric	Count
Definitions `toContinuousAddEquiv`, `ContinuousAddEquiv`, `symm_apply`, `instEquivLike`, `instInhabited`, `instUnique`, `mk'`, `ofUnique`, `refl`, `toAddEquiv`, `toHomeomorph`, `trans`, `ContinuousAddMonoidHom`, `add`, `comp`, `coprod`, `diag`, `fst`, `id`, `inl`, `inr`, `instAddCommGroup`, `instAddCommMonoid`, `instCoeOutOfAddMonoidHomClassOfContinuousMapClass`, `instFunLike`, `instInhabited`, `instZero`, `neg`, `ofClass`, `prod`, `prodMap`, `snd`, `swap`, `toAddMonoidHom`, `toContinuousAddMonoidHom`, `toContinuousMap`, `ContinuousMonoidHom`, `comp`, `coprod`, `diag`, `fst`, `id`, `inl`, `inr`, `instCoeOutOfMonoidHomClassOfContinuousMapClass`, `instCommGroup`, `instCommMonoid`, `instFunLike`, `instInhabited`, `instOne`, `inv`, `mul`, `ofClass`, `prod`, `prodMap`, `snd`, `swap`, `toContinuousMap`, `toContinuousMonoidHom`, `toMonoidHom`, `«term_→ₜ_»`, `«term_→ₜ+_»`, `ContinuousMulEquiv`, `symm_apply`, `instEquivLike`, `instInhabited`, `instUnique`, `mk'`, `ofUnique`, `refl`, `toHomeomorph`, `toMulEquiv`, `trans`, `toContinuousMulEquiv`, `«term_≃ₜ_»`, `«term_≃ₜ+_»`	76
Theorems `symm_toContinuousAddEquiv`, `toAddEquiv_toContinuousAddEquiv`, `toContinuousAddEquiv_apply`, `toContinuousAddEquiv_symm_apply`, `toHomeomorph_toContinuousAddEquiv`, `apply_eq_iff_eq`, `apply_eq_iff_symm_apply`, `apply_symm_apply`, `bijective`, `coe_mk`, `coe_refl`, `coe_toHomeomorph_symm`, `coe_trans`, `comp_symm_eq`, `continuous_invFun`, `continuous_toFun`, `eq_comp_symm`, `eq_symm_apply`, `eq_symm_comp`, `equivLike_neg_eq_symm`, `ext`, `ext_iff`, `injective`, `instAddEquivClass`, `instHomeomorphClass`, `invFun_eq_symm`, `refl_apply`, `self_comp_symm`, `self_trans_symm`, `surjective`, `symm_apply_apply`, `symm_apply_eq`, `symm_bijective`, `symm_comp_eq`, `symm_comp_self`, `symm_symm`, `symm_trans_apply`, `symm_trans_self`, `toAddEquiv_eq_coe`, `toEquiv_eq_coe`, `toHomeomorph_eq_coe`, `trans_apply`, `add_apply`, `add_toFun`, `coe_coe`, `coe_comp`, `coe_id`, `coe_toAddMonoidHom`, `coe_toContinuousMap`, `coe_zero`, `comp_toFun`, `continuous_toFun`, `coprod_toFun`, `diag_toFun`, `ext`, `ext_iff`, `fst_toFun`, `id_toFun`, `inl_toFun`, `inr_toFun`, `instAddMonoidHomClass`, `instContinuousMapClass`, `neg_toFun`, `nsmul_apply`, `prodMap_toFun`, `prod_toFun`, `snd_toFun`, `swap_toFun`, `toAddMonoidHom_injective`, `toAddMonoidHom_toContinuousAddMonoidHom`, `toContinuousMap_injective`, `toContinuousMap_toContinuousAddMonoidHom`, `zero_toFun`, `coe_coe`, `coe_comp`, `coe_id`, `coe_one`, `coe_toContinuousMap`, `coe_toMonoidHom`, `comp_toFun`, `continuous_toFun`, `coprod_toFun`, `diag_toFun`, `ext`, `ext_iff`, `fst_toFun`, `id_toFun`, `inl_toFun`, `inr_toFun`, `instContinuousMapClass`, `instMonoidHomClass`, `inv_toFun`, `mul_apply`, `mul_toFun`, `one_toFun`, `pow_apply`, `prodMap_toFun`, `prod_toFun`, `snd_toFun`, `swap_toFun`, `toContinuousMap_injective`, `toContinuousMap_toContinuousMonoidHom`, `toMonoidHom_injective`, `toMonoidHom_toContinuousMonoidHom`, `apply_eq_iff_eq`, `apply_eq_iff_symm_apply`, `apply_symm_apply`, `bijective`, `coe_mk`, `coe_mk'`, `coe_refl`, `coe_toHomeomorph_symm`, `coe_trans`, `comp_symm_eq`, `continuous_invFun`, `continuous_toFun`, `eq_comp_symm`, `eq_symm_apply`, `eq_symm_comp`, `equivLike_inv_eq_symm`, `ext`, `ext_iff`, `injective`, `instHomeomorphClass`, `instMulEquivClass`, `invFun_eq_symm`, `refl_apply`, `self_comp_symm`, `self_trans_symm`, `surjective`, `symm_apply_apply`, `symm_apply_eq`, `symm_bijective`, `symm_comp_eq`, `symm_comp_self`, `symm_symm`, `symm_trans_apply`, `symm_trans_self`, `toEquiv_eq_coe`, `toHomeomorph_eq_coe`, `toMulEquiv_eq_coe`, `trans_apply`, `symm_toContinuousMulEquiv`, `toContinuousMulEquiv_apply`, `toContinuousMulEquiv_symm_apply`, `toHomeomorph_toContinuousMulEquiv`, `toMulEquiv_toContinuousMulEquiv`	147
Total	223

AddEquiv

Definitions

Name	Category	Theorems
`toContinuousAddEquiv` 📖	CompOp	5 math math: `toHomeomorph_toContinuousAddEquiv`, `toContinuousAddEquiv_apply`, `toAddEquiv_toContinuousAddEquiv`, `symm_toContinuousAddEquiv`, `toContinuousAddEquiv_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`symm_toContinuousAddEquiv` 📖	mathematical	`IsOpen` `Set.preimage` `DFunLike.coe` `AddEquiv` `EquivLike.toFunLike` `instEquivLike`	`ContinuousAddEquiv.symm` `toContinuousAddEquiv` `symm`	—	—
`toAddEquiv_toContinuousAddEquiv` 📖	mathematical	`IsOpen` `Set.preimage` `DFunLike.coe` `AddEquiv` `EquivLike.toFunLike` `instEquivLike`	`AddEquivClass.toAddEquiv` `ContinuousAddEquiv` `ContinuousAddEquiv.instEquivLike` `ContinuousAddEquiv.instAddEquivClass` `toContinuousAddEquiv`	—	`ContinuousAddEquiv.instAddEquivClass`
`toContinuousAddEquiv_apply` 📖	mathematical	`IsOpen` `Set.preimage` `DFunLike.coe` `AddEquiv` `EquivLike.toFunLike` `instEquivLike`	`ContinuousAddEquiv` `ContinuousAddEquiv.instEquivLike` `toContinuousAddEquiv`	—	—
`toContinuousAddEquiv_symm_apply` 📖	mathematical	`IsOpen` `Set.preimage` `DFunLike.coe` `AddEquiv` `EquivLike.toFunLike` `instEquivLike`	`ContinuousAddEquiv` `ContinuousAddEquiv.instEquivLike` `ContinuousAddEquiv.symm` `toContinuousAddEquiv` `symm`	—	—
`toHomeomorph_toContinuousAddEquiv` 📖	mathematical	`IsOpen` `Set.preimage` `DFunLike.coe` `AddEquiv` `EquivLike.toFunLike` `instEquivLike`	`HomeomorphClass.toHomeomorph` `ContinuousAddEquiv` `ContinuousAddEquiv.instEquivLike` `ContinuousAddEquiv.instHomeomorphClass` `toContinuousAddEquiv` `Equiv.toHomeomorph` `toEquiv`	—	`ContinuousAddEquiv.instHomeomorphClass`

ContinuousAddEquiv

Definitions

Name	Category	Theorems
`instEquivLike` 📖	CompOp	44 math math: `AddSubgroup.addSubgroupOfContinuousAddEquivOfLe_apply`, `eq_comp_symm`, `symm_comp_eq`, `instAddEquivClass`, `coe_refl`, `instHomeomorphClass`, `MeasureTheory.addEquivAddHaarChar_smul_preimage`, `AddEquiv.toHomeomorph_toContinuousAddEquiv`, `MeasureTheory.addEquivAddHaarChar_eq`, `AddEquiv.toContinuousAddEquiv_apply`, `AddEquiv.toAddEquiv_toContinuousAddEquiv`, `surjective`, `MeasureTheory.integral_comap_eq_addEquivAddHaarChar_smul`, `symm_apply_eq`, `toEquiv_eq_coe`, `eq_symm_comp`, `symm_comp_self`, `self_comp_symm`, `toHomeomorph_eq_coe`, `isAddHaarMeasure_map`, `MeasureTheory.addEquivAddHaarChar_smul_map`, `apply_eq_iff_eq`, `toAddEquiv_eq_coe`, `invFun_eq_symm`, `ext_iff`, `MeasureTheory.addEquivAddHaarChar_smul_eq_comap`, `injective`, `eq_symm_apply`, `coe_mk`, `apply_eq_iff_symm_apply`, `AddSubgroup.addSubgroupOfContinuousAddEquivOfLe_symm_apply`, `symm_apply_apply`, `bijective`, `AddSubgroup.addSubgroupOfContinuousAddEquivOfLe_toAddEquiv`, `comp_symm_eq`, `refl_apply`, `equivLike_neg_eq_symm`, `AddEquiv.toContinuousAddEquiv_symm_apply`, `MeasureTheory.addEquivAddHaarChar_smul_integral_map`, `coe_trans`, `apply_symm_apply`, `trans_apply`, `coe_toHomeomorph_symm`, `symm_trans_apply`
`instInhabited` 📖	CompOp	—
`instUnique` 📖	CompOp	—
`mk'` 📖	CompOp	—
`ofUnique` 📖	CompOp	—
`refl` 📖	CompOp	5 math math: `coe_refl`, `self_trans_symm`, `MeasureTheory.addEquivAddHaarChar_refl`, `symm_trans_self`, `refl_apply`
`toAddEquiv` 📖	CompOp	5 math math: `continuous_toFun`, `toEquiv_eq_coe`, `continuous_invFun`, `toAddEquiv_eq_coe`, `invFun_eq_symm`
`toHomeomorph` 📖	CompOp	1 math math: `toHomeomorph_eq_coe`
`trans` 📖	CompOp	6 math math: `self_trans_symm`, `symm_trans_self`, `MeasureTheory.addEquivAddHaarChar_trans`, `coe_trans`, `trans_apply`, `symm_trans_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_eq_iff_eq` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`injective`
`apply_eq_iff_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.apply_eq_iff_eq_symm_apply`
`apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.apply_symm_apply`
`bijective` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`EquivLike.bijective`
`coe_mk` 📖	mathematical	`Continuous` `Equiv.toFun` `AddEquiv.toEquiv` `Equiv.invFun`	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike` `AddEquiv` `AddEquiv.instEquivLike`	—	—
`coe_refl` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike` `refl`	—	—
`coe_toHomeomorph_symm` 📖	mathematical	—	`Homeomorph.symm` `HomeomorphClass.toHomeomorph` `ContinuousAddEquiv` `instEquivLike` `instHomeomorphClass` `symm`	—	`instHomeomorphClass`
`coe_trans` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike` `trans`	—	—
`comp_symm_eq` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.comp_symm_eq`
`continuous_invFun` 📖	mathematical	—	`Continuous` `Equiv.invFun` `AddEquiv.toEquiv` `toAddEquiv`	—	—
`continuous_toFun` 📖	mathematical	—	`Continuous` `Equiv.toFun` `AddEquiv.toEquiv` `toAddEquiv`	—	—
`eq_comp_symm` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.eq_comp_symm`
`eq_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.eq_symm_apply`
`eq_symm_comp` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.eq_symm_comp`
`equivLike_neg_eq_symm` 📖	mathematical	—	`EquivLike.inv` `ContinuousAddEquiv` `instEquivLike` `DFunLike.coe` `EquivLike.toFunLike` `symm`	—	—
`ext` 📖	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`ext`
`injective` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`EquivLike.injective`
`instAddEquivClass` 📖	mathematical	—	`AddEquivClass` `ContinuousAddEquiv` `instEquivLike`	—	`AddEquiv.map_add'`
`instHomeomorphClass` 📖	mathematical	—	`HomeomorphClass` `ContinuousAddEquiv` `instEquivLike`	—	`continuous_toFun` `continuous_invFun`
`invFun_eq_symm` 📖	mathematical	—	`Equiv.invFun` `AddEquiv.toEquiv` `toAddEquiv` `DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—
`refl_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike` `refl`	—	—
`self_comp_symm` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`apply_symm_apply`
`self_trans_symm` 📖	mathematical	—	`trans` `symm` `refl`	—	`DFunLike.ext` `symm_apply_apply`
`surjective` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`EquivLike.surjective`
`symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.symm_apply_apply`
`symm_apply_eq` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.symm_apply_eq`
`symm_bijective` 📖	mathematical	—	`Function.Bijective` `ContinuousAddEquiv` `symm`	—	`Function.bijective_iff_has_inverse` `symm_symm`
`symm_comp_eq` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.symm_comp_eq`
`symm_comp_self` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`symm_apply_apply`
`symm_symm` 📖	mathematical	—	`symm`	—	—
`symm_trans_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike` `symm` `trans`	—	—
`symm_trans_self` 📖	mathematical	—	`trans` `symm` `refl`	—	`DFunLike.ext` `apply_symm_apply`
`toAddEquiv_eq_coe` 📖	mathematical	—	`toAddEquiv` `AddEquivClass.toAddEquiv` `ContinuousAddEquiv` `instEquivLike` `instAddEquivClass`	—	—
`toEquiv_eq_coe` 📖	mathematical	—	`AddEquiv.toEquiv` `toAddEquiv` `EquivLike.toEquiv` `ContinuousAddEquiv` `instEquivLike`	—	—
`toHomeomorph_eq_coe` 📖	mathematical	—	`toHomeomorph` `HomeomorphClass.toHomeomorph` `ContinuousAddEquiv` `instEquivLike` `instHomeomorphClass`	—	—
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddEquiv` `EquivLike.toFunLike` `instEquivLike` `trans`	—	—

ContinuousAddEquiv.Simps

Definitions

Name	Category	Theorems
`symm_apply` 📖	CompOp	—

ContinuousAddMonoidHom

Definitions

Name	Category	Theorems
`add` 📖	CompOp	1 math math: `add_toFun`
`comp` 📖	CompOp	9 math math: `continuous_comp`, `coe_comp`, `ProfiniteAddGrp.ofHom_comp`, `continuous_comp_right`, `ContinuousLinearMap.toContinuousAddMonoidHom_comp`, `lp.ext_continuousAddMonoidHom_iff`, `comp_toFun`, `ProfiniteAddGrp.hom_comp`, `continuous_comp_left`
`coprod` 📖	CompOp	1 math math: `coprod_toFun`
`diag` 📖	CompOp	1 math math: `diag_toFun`
`fst` 📖	CompOp	1 math math: `fst_toFun`
`id` 📖	CompOp	5 math math: `coe_id`, `ProfiniteAddGrp.ofHom_id`, `ProfiniteAddGrp.hom_id`, `ContinuousLinearMap.toContinuousAddMonoidHom_id`, `id_toFun`
`inl` 📖	CompOp	1 math math: `inl_toFun`
`inr` 📖	CompOp	1 math math: `inr_toFun`
`instAddCommGroup` 📖	CompOp	3 math math: `ContinuousLinearMap.toContinuousAddMonoidHom_neg`, `instIsTopologicalAddGroup`, `ContinuousLinearMap.toContinuousAddMonoidHom_sub`
`instAddCommMonoid` 📖	CompOp	3 math math: `ContinuousLinearMap.toContinuousAddMonoidHom_add`, `nsmul_apply`, `add_apply`
`instCoeOutOfAddMonoidHomClassOfContinuousMapClass` 📖	CompOp	—
`instFunLike` 📖	CompOp	43 math math: `coe_id`, `snd_toFun`, `prodMap_toFun`, `instAddMonoidHomClass`, `ProfiniteAddGrp.ofHom_apply`, `ProfiniteAddGrp.instFaithfulProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap`, `coe_comp`, `ProfiniteAddGrp.instPreservesLimitsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap`, `ProfiniteAddGrp.hom_neg_apply`, `nsmul_apply`, `ProfiniteAddGrp.neg_hom_apply`, `inl_toFun`, `ProfiniteAddGrp.comp_apply`, `instContinuousEvalConst`, `toContinuousMap_toContinuousAddMonoidHom`, `lp.singleContinuousAddMonoidHom_apply`, `ProfiniteAddGrp.instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap`, `ProfiniteAddGrp.id_apply`, `coe_toContinuousMap`, `LinearMap.IsSymmetric.toSelfAdjoint_apply`, `ProfiniteAddGrp.coe_id`, `zero_toFun`, `ext_iff`, `prod_toFun`, `coprod_toFun`, `coe_zero`, `toAddMonoidHom_toContinuousAddMonoidHom`, `neg_toFun`, `coe_coe`, `fst_toFun`, `ProfiniteAddGrp.coe_comp`, `isClosedEmbedding_coe`, `SeparationQuotient.liftNormedAddGroupHom_apply`, `diag_toFun`, `add_toFun`, `add_apply`, `comp_toFun`, `inr_toFun`, `id_toFun`, `coe_toAddMonoidHom`, `instContinuousEval`, `instContinuousMapClass`, `swap_toFun`
`instInhabited` 📖	CompOp	—
`instZero` 📖	CompOp	3 math math: `ContinuousLinearMap.toContinuousAddMonoidHom_zero`, `zero_toFun`, `coe_zero`
`neg` 📖	CompOp	1 math math: `neg_toFun`
`ofClass` 📖	CompOp	—
`prod` 📖	CompOp	1 math math: `prod_toFun`
`prodMap` 📖	CompOp	1 math math: `prodMap_toFun`
`snd` 📖	CompOp	1 math math: `snd_toFun`
`swap` 📖	CompOp	1 math math: `swap_toFun`
`toAddMonoidHom` 📖	CompOp	3 math math: `toAddMonoidHom_injective`, `coe_toAddMonoidHom`, `continuous_toFun`
`toContinuousAddMonoidHom` 📖	CompOp	14 math math: `ContinuousLinearMap.toContinuousAddMonoidHom_add`, `toContinuousMap_toContinuousAddMonoidHom`, `ContinuousLinearMap.toContinuousAddMonoidHom_zero`, `ContinuousLinearMap.toContinuousAddMonoidHom_comp`, `LinearMap.IsSymmetric.toSelfAdjoint_apply`, `ContinuousLinearMap.toContinuousAddMonoidHom_injective`, `ContinuousLinearMap.toContinuousAddMonoidHom_inj`, `toAddMonoidHom_toContinuousAddMonoidHom`, `ContinuousLinearMap.toContinuousAddMonoidHom_neg`, `coe_coe`, `ContinuousLinearMap.toContinuousAddMonoidHom_restrictScalars`, `ContinuousLinearMap.toContinuousAddMonoidHom_id`, `ContinuousLinearMap.toContinuousAddMonoidHom_sub`, `SeparationQuotient.liftNormedAddGroupHom_apply`
`toContinuousMap` 📖	CompOp	6 math math: `range_toContinuousMap`, `coe_toContinuousMap`, `isClosedEmbedding_toContinuousMap`, `isInducing_toContinuousMap`, `isEmbedding_toContinuousMap`, `toContinuousMap_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `AddCommMonoid.toAddMonoid` `instFunLike` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddCommMonoid`	—	—
`add_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `Prod.instAddMonoid` `AddCommMonoid.toAddMonoid` `instTopologicalSpaceProd` `instFunLike` `add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—
`coe_coe` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `instFunLike` `toContinuousAddMonoidHom`	—	—
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `instFunLike` `comp`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `instFunLike` `id`	—	—
`coe_toAddMonoidHom` 📖	mathematical	—	`toAddMonoidHom` `AddMonoidHomClass.toAddMonoidHom` `ContinuousAddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instFunLike` `instAddMonoidHomClass`	—	—
`coe_toContinuousMap` 📖	mathematical	—	`toContinuousMap` `toContinuousMap` `ContinuousAddMonoidHom` `instFunLike` `instContinuousMapClass`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `instFunLike` `instZero` `Pi.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—
`comp_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `instFunLike` `comp`	—	—
`continuous_toFun` 📖	mathematical	—	`Continuous` `ZeroHom.toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.toZeroHom` `toAddMonoidHom`	—	—
`coprod_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `Prod.instAddMonoid` `AddCommMonoid.toAddMonoid` `instTopologicalSpaceProd` `instFunLike` `coprod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—
`diag_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `Prod.instAddMonoid` `instTopologicalSpaceProd` `instFunLike` `diag`	—	—
`ext` 📖	—	`DFunLike.coe` `ContinuousAddMonoidHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `instFunLike`	—	`ext`
`fst_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `Prod.instAddMonoid` `instTopologicalSpaceProd` `instFunLike` `fst`	—	—
`id_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `instFunLike` `id`	—	—
`inl_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `Prod.instAddMonoid` `instTopologicalSpaceProd` `instFunLike` `inl` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—
`inr_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `Prod.instAddMonoid` `instTopologicalSpaceProd` `instFunLike` `inr` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—
`instAddMonoidHomClass` 📖	mathematical	—	`AddMonoidHomClass` `ContinuousAddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instFunLike`	—	`AddMonoidHom.map_add'` `ZeroHom.map_zero'`
`instContinuousMapClass` 📖	mathematical	—	`ContinuousMapClass` `ContinuousAddMonoidHom` `instFunLike`	—	`continuous_toFun`
`neg_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instFunLike` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`nsmul_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `AddCommMonoid.toAddMonoid` `instFunLike` `AddMonoid.toNatSMul` `instAddCommMonoid`	—	`zero_nsmul` `zero_toFun` `succ_nsmul` `add_apply`
`prodMap_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `Prod.instAddMonoid` `instTopologicalSpaceProd` `instFunLike` `prodMap`	—	—
`prod_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `Prod.instAddMonoid` `instTopologicalSpaceProd` `instFunLike` `prod`	—	—
`snd_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `Prod.instAddMonoid` `instTopologicalSpaceProd` `instFunLike` `snd`	—	—
`swap_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `Prod.instAddMonoid` `instTopologicalSpaceProd` `instFunLike` `swap`	—	—
`toAddMonoidHom_injective` 📖	mathematical	—	`ContinuousAddMonoidHom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `toAddMonoidHom`	—	`ext` `DFunLike.ext_iff`
`toAddMonoidHom_toContinuousAddMonoidHom` 📖	mathematical	—	`AddMonoidHomClass.toAddMonoidHom` `ContinuousAddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instFunLike` `instAddMonoidHomClass` `toContinuousAddMonoidHom`	—	`instAddMonoidHomClass`
`toContinuousMap_injective` 📖	mathematical	—	`ContinuousAddMonoidHom` `ContinuousMap` `toContinuousMap`	—	`ext` `DFunLike.ext_iff`
`toContinuousMap_toContinuousAddMonoidHom` 📖	mathematical	—	`toContinuousMap` `ContinuousAddMonoidHom` `instFunLike` `instContinuousMapClass` `toContinuousAddMonoidHom`	—	`instContinuousMapClass`
`zero_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousAddMonoidHom` `instFunLike` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—

ContinuousMonoidHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	10 math math: `ProfiniteGrp.ofHom_comp`, `ProfiniteGrp.hom_comp`, `ContAction.resComp_hom`, `continuous_comp_left`, `continuous_comp_right`, `comp_toFun`, `coe_comp`, `continuous_comp`, `PontryaginDual.map_comp`, `ContAction.resComp_inv`
`coprod` 📖	CompOp	1 math math: `coprod_toFun`
`diag` 📖	CompOp	1 math math: `diag_toFun`
`fst` 📖	CompOp	1 math math: `fst_toFun`
`id` 📖	CompOp	4 math math: `ProfiniteGrp.hom_id`, `coe_id`, `id_toFun`, `ProfiniteGrp.ofHom_id`
`inl` 📖	CompOp	1 math math: `inl_toFun`
`inr` 📖	CompOp	1 math math: `inr_toFun`
`instCoeOutOfMonoidHomClassOfContinuousMapClass` 📖	CompOp	—
`instCommGroup` 📖	CompOp	2 math math: `instIsTopologicalGroup`, `PontryaginDual.map_mul`
`instCommMonoid` 📖	CompOp	2 math math: `mul_apply`, `pow_apply`
`instFunLike` 📖	CompOp	54 math math: `toContinuousMap_toContinuousMonoidHom`, `ProfiniteGrp.instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap`, `ProfiniteGrp.ProfiniteCompletion.lift_eta`, `coe_toContinuousMap`, `ProfiniteGrp.coe_id`, `ProfiniteGrp.ProfiniteCompletion.lift_eta_assoc`, `ProfiniteGrp.instFaithfulProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap`, `ProfiniteGrp.toLimit_surjective`, `swap_toFun`, `coe_id`, `snd_toFun`, `ProfiniteGrp.denseRange_toLimit`, `ProfiniteGrp.comp_apply`, `mul_toFun`, `ext_iff`, `ProfiniteGrp.inv_hom_apply`, `inv_toFun`, `ContAction.resCongr_hom`, `ContAction.res_obj_obj`, `coe_toMonoidHom`, `instContinuousMapClass`, `instContinuousEvalConst`, `id_toFun`, `ProfiniteGrp.hom_inv_apply`, `instMonoidHomClass`, `coe_one`, `instContinuousEval`, `mul_apply`, `pow_apply`, `diag_toFun`, `comp_toFun`, `ProfiniteGrp.toLimit_injective`, `ProfiniteGrp.ofHom_apply`, `coe_comp`, `ContAction.resCongr_inv`, `inl_toFun`, `PontryaginDual.map_apply`, `ProfiniteGrp.coe_comp`, `coe_coe`, `inr_toFun`, `coprod_toFun`, `ProfiniteGrp.diagram_map`, `prod_toFun`, `ProfiniteGrp.id_apply`, `one_toFun`, `fst_toFun`, `ProfiniteGrp.instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap`, `ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap`, `ContAction.res_map`, `prodMap_toFun`, `isClosedEmbedding_coe`, `toMonoidHom_toContinuousMonoidHom`, `ProfiniteGrp.diagram_obj`, `ProfiniteGrp.instReflectsIsomorphismsForgetContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite`
`instInhabited` 📖	CompOp	—
`instOne` 📖	CompOp	3 math math: `PontryaginDual.map_one`, `coe_one`, `one_toFun`
`inv` 📖	CompOp	1 math math: `inv_toFun`
`mul` 📖	CompOp	1 math math: `mul_toFun`
`ofClass` 📖	CompOp	—
`prod` 📖	CompOp	1 math math: `prod_toFun`
`prodMap` 📖	CompOp	1 math math: `prodMap_toFun`
`snd` 📖	CompOp	1 math math: `snd_toFun`
`swap` 📖	CompOp	1 math math: `swap_toFun`
`toContinuousMap` 📖	CompOp	6 math math: `isInducing_toContinuousMap`, `coe_toContinuousMap`, `toContinuousMap_injective`, `isEmbedding_toContinuousMap`, `isClosedEmbedding_toContinuousMap`, `range_toContinuousMap`
`toContinuousMonoidHom` 📖	CompOp	5 math math: `toContinuousMap_toContinuousMonoidHom`, `ContAction.resEquiv_inverse`, `ContAction.resEquiv_functor`, `coe_coe`, `toMonoidHom_toContinuousMonoidHom`
`toMonoidHom` 📖	CompOp	3 math math: `toMonoidHom_injective`, `coe_toMonoidHom`, `continuous_toFun`
`«term_→ₜ*_»` 📖	CompOp	—
`«term_→ₜ+_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_coe` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `instFunLike` `toContinuousMonoidHom`	—	—
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `instFunLike` `comp`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `instFunLike` `id`	—	—
`coe_one` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `instFunLike` `instOne` `Pi.instOne` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`coe_toContinuousMap` 📖	mathematical	—	`toContinuousMap` `toContinuousMap` `ContinuousMonoidHom` `instFunLike` `instContinuousMapClass`	—	—
`coe_toMonoidHom` 📖	mathematical	—	`toMonoidHom` `MonoidHomClass.toMonoidHom` `ContinuousMonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instFunLike` `instMonoidHomClass`	—	—
`comp_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `instFunLike` `comp`	—	—
`continuous_toFun` 📖	mathematical	—	`Continuous` `OneHom.toFun` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.toOneHom` `toMonoidHom`	—	—
`coprod_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `Prod.instMonoid` `CommMonoid.toMonoid` `instTopologicalSpaceProd` `instFunLike` `coprod` `CommMagma.toMul` `CommSemigroup.toCommMagma` `CommMonoid.toCommSemigroup`	—	—
`diag_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `Prod.instMonoid` `instTopologicalSpaceProd` `instFunLike` `diag`	—	—
`ext` 📖	—	`DFunLike.coe` `ContinuousMonoidHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `instFunLike`	—	`ext`
`fst_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `Prod.instMonoid` `instTopologicalSpaceProd` `instFunLike` `fst`	—	—
`id_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `instFunLike` `id`	—	—
`inl_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `Prod.instMonoid` `instTopologicalSpaceProd` `instFunLike` `inl` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`inr_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `Prod.instMonoid` `instTopologicalSpaceProd` `instFunLike` `inr` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`instContinuousMapClass` 📖	mathematical	—	`ContinuousMapClass` `ContinuousMonoidHom` `instFunLike`	—	`continuous_toFun`
`instMonoidHomClass` 📖	mathematical	—	`MonoidHomClass` `ContinuousMonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instFunLike`	—	`MonoidHom.map_mul'` `OneHom.map_one'`
`inv_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instFunLike` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	—
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `CommMonoid.toMonoid` `instFunLike` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instCommMonoid`	—	—
`mul_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `Prod.instMonoid` `CommMonoid.toMonoid` `instTopologicalSpaceProd` `instFunLike` `mul` `CommMagma.toMul` `CommSemigroup.toCommMagma` `CommMonoid.toCommSemigroup`	—	—
`one_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `instFunLike` `instOne` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`pow_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `CommMonoid.toMonoid` `instFunLike` `Monoid.toNatPow` `instCommMonoid`	—	`pow_zero` `one_toFun` `pow_succ` `mul_apply`
`prodMap_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `Prod.instMonoid` `instTopologicalSpaceProd` `instFunLike` `prodMap`	—	—
`prod_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `Prod.instMonoid` `instTopologicalSpaceProd` `instFunLike` `prod`	—	—
`snd_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `Prod.instMonoid` `instTopologicalSpaceProd` `instFunLike` `snd`	—	—
`swap_toFun` 📖	mathematical	—	`DFunLike.coe` `ContinuousMonoidHom` `Prod.instMonoid` `instTopologicalSpaceProd` `instFunLike` `swap`	—	—
`toContinuousMap_injective` 📖	mathematical	—	`ContinuousMonoidHom` `ContinuousMap` `toContinuousMap`	—	`ext` `DFunLike.ext_iff`
`toContinuousMap_toContinuousMonoidHom` 📖	mathematical	—	`toContinuousMap` `ContinuousMonoidHom` `instFunLike` `instContinuousMapClass` `toContinuousMonoidHom`	—	`instContinuousMapClass`
`toMonoidHom_injective` 📖	mathematical	—	`ContinuousMonoidHom` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `toMonoidHom`	—	`ext` `DFunLike.ext_iff`
`toMonoidHom_toContinuousMonoidHom` 📖	mathematical	—	`MonoidHomClass.toMonoidHom` `ContinuousMonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instFunLike` `instMonoidHomClass` `toContinuousMonoidHom`	—	`instMonoidHomClass`

ContinuousMulEquiv

Definitions

Name	Category	Theorems
`instEquivLike` 📖	CompOp	49 math math: `MeasureTheory.mulEquivHaarChar_smul_integral_map`, `coe_refl`, `instHomeomorphClass`, `surjective`, `Subgroup.subgroupOfContinuousMulEquivOfLe_toMulEquiv`, `MulEquiv.toContinuousMulEquiv_symm_apply`, `coe_trans`, `MulEquiv.toMulEquiv_toContinuousMulEquiv`, `MeasureTheory.mulEquivHaarChar_eq`, `eq_comp_symm`, `symm_apply_eq`, `symm_comp_self`, `eq_symm_apply`, `ContAction.resEquiv_inverse`, `MulEquiv.toContinuousMulEquiv_apply`, `eq_symm_comp`, `MeasureTheory.mulEquivHaarChar_smul_map`, `symm_trans_apply`, `invFun_eq_symm`, `coe_mk'`, `MulEquiv.toHomeomorph_toContinuousMulEquiv`, `symm_apply_apply`, `apply_symm_apply`, `toMulEquiv_eq_coe`, `ContAction.resEquiv_functor`, `coe_mk`, `Subgroup.subgroupOfContinuousMulEquivOfLe_apply`, `self_comp_symm`, `instMulEquivClass`, `apply_eq_iff_eq`, `ext_iff`, `isHaarMeasure_map`, `Units.toMulEquiv_mapContinuousMulEquiv`, `MeasureTheory.mulEquivHaarChar_smul_preimage`, `Subgroup.subgroupOfContinuousMulEquivOfLe_symm_apply`, `injective`, `trans_apply`, `MeasureTheory.mulEquivHaarChar_smul_eq_comap`, `refl_apply`, `equivLike_inv_eq_symm`, `symm_comp_eq`, `coe_toHomeomorph_symm`, `toEquiv_eq_coe`, `toHomeomorph_eq_coe`, `bijective`, `apply_eq_iff_symm_apply`, `Units.mapContinuousMulEquiv_apply`, `MeasureTheory.integral_comap_eq_mulEquivHaarChar_smul`, `comp_symm_eq`
`instInhabited` 📖	CompOp	—
`instUnique` 📖	CompOp	—
`mk'` 📖	CompOp	1 math math: `coe_mk'`
`ofUnique` 📖	CompOp	—
`refl` 📖	CompOp	5 math math: `coe_refl`, `symm_trans_self`, `MeasureTheory.mulEquivHaarChar_refl`, `self_trans_symm`, `refl_apply`
`toHomeomorph` 📖	CompOp	1 math math: `toHomeomorph_eq_coe`
`toMulEquiv` 📖	CompOp	5 math math: `continuous_toFun`, `invFun_eq_symm`, `continuous_invFun`, `toMulEquiv_eq_coe`, `toEquiv_eq_coe`
`trans` 📖	CompOp	6 math math: `symm_trans_self`, `coe_trans`, `symm_trans_apply`, `MeasureTheory.mulEquivHaarChar_trans`, `self_trans_symm`, `trans_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_eq_iff_eq` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`injective`
`apply_eq_iff_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.apply_eq_iff_eq_symm_apply`
`apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.apply_symm_apply`
`bijective` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`EquivLike.bijective`
`coe_mk` 📖	mathematical	`Continuous` `Equiv.toFun` `MulEquiv.toEquiv` `Equiv.invFun`	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike` `MulEquiv` `MulEquiv.instEquivLike`	—	—
`coe_mk'` 📖	mathematical	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	`ContinuousMulEquiv` `instEquivLike` `mk'`	—	—
`coe_refl` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike` `refl`	—	—
`coe_toHomeomorph_symm` 📖	mathematical	—	`Homeomorph.symm` `HomeomorphClass.toHomeomorph` `ContinuousMulEquiv` `instEquivLike` `instHomeomorphClass` `symm`	—	`instHomeomorphClass`
`coe_trans` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike` `trans`	—	—
`comp_symm_eq` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.comp_symm_eq`
`continuous_invFun` 📖	mathematical	—	`Continuous` `Equiv.invFun` `MulEquiv.toEquiv` `toMulEquiv`	—	—
`continuous_toFun` 📖	mathematical	—	`Continuous` `Equiv.toFun` `MulEquiv.toEquiv` `toMulEquiv`	—	—
`eq_comp_symm` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.eq_comp_symm`
`eq_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.eq_symm_apply`
`eq_symm_comp` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.eq_symm_comp`
`equivLike_inv_eq_symm` 📖	mathematical	—	`EquivLike.inv` `ContinuousMulEquiv` `instEquivLike` `DFunLike.coe` `EquivLike.toFunLike` `symm`	—	—
`ext` 📖	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`ext`
`injective` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`EquivLike.injective`
`instHomeomorphClass` 📖	mathematical	—	`HomeomorphClass` `ContinuousMulEquiv` `instEquivLike`	—	`continuous_toFun` `continuous_invFun`
`instMulEquivClass` 📖	mathematical	—	`MulEquivClass` `ContinuousMulEquiv` `instEquivLike`	—	`MulEquiv.map_mul'`
`invFun_eq_symm` 📖	mathematical	—	`Equiv.invFun` `MulEquiv.toEquiv` `toMulEquiv` `DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—
`refl_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike` `refl`	—	—
`self_comp_symm` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`apply_symm_apply`
`self_trans_symm` 📖	mathematical	—	`trans` `symm` `refl`	—	`DFunLike.ext` `symm_apply_apply`
`surjective` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike`	—	`EquivLike.surjective`
`symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.symm_apply_apply`
`symm_apply_eq` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.symm_apply_eq`
`symm_bijective` 📖	mathematical	—	`Function.Bijective` `ContinuousMulEquiv` `symm`	—	`Function.bijective_iff_has_inverse` `symm_symm`
`symm_comp_eq` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Equiv.symm_comp_eq`
`symm_comp_self` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`symm_apply_apply`
`symm_symm` 📖	mathematical	—	`symm`	—	—
`symm_trans_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike` `symm` `trans`	—	—
`symm_trans_self` 📖	mathematical	—	`trans` `symm` `refl`	—	`DFunLike.ext` `apply_symm_apply`
`toEquiv_eq_coe` 📖	mathematical	—	`MulEquiv.toEquiv` `toMulEquiv` `EquivLike.toEquiv` `ContinuousMulEquiv` `instEquivLike`	—	—
`toHomeomorph_eq_coe` 📖	mathematical	—	`toHomeomorph` `HomeomorphClass.toHomeomorph` `ContinuousMulEquiv` `instEquivLike` `instHomeomorphClass`	—	—
`toMulEquiv_eq_coe` 📖	mathematical	—	`toMulEquiv` `MulEquivClass.toMulEquiv` `ContinuousMulEquiv` `instEquivLike` `instMulEquivClass`	—	—
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMulEquiv` `EquivLike.toFunLike` `instEquivLike` `trans`	—	—

ContinuousMulEquiv.Simps

Definitions

Name	Category	Theorems
`symm_apply` 📖	CompOp	—

MulEquiv

Definitions

Name	Category	Theorems
`toContinuousMulEquiv` 📖	CompOp	5 math math: `toContinuousMulEquiv_symm_apply`, `toMulEquiv_toContinuousMulEquiv`, `toContinuousMulEquiv_apply`, `toHomeomorph_toContinuousMulEquiv`, `symm_toContinuousMulEquiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`symm_toContinuousMulEquiv` 📖	mathematical	`IsOpen` `Set.preimage` `DFunLike.coe` `MulEquiv` `EquivLike.toFunLike` `instEquivLike`	`ContinuousMulEquiv.symm` `toContinuousMulEquiv` `symm`	—	—
`toContinuousMulEquiv_apply` 📖	mathematical	`IsOpen` `Set.preimage` `DFunLike.coe` `MulEquiv` `EquivLike.toFunLike` `instEquivLike`	`ContinuousMulEquiv` `ContinuousMulEquiv.instEquivLike` `toContinuousMulEquiv`	—	—
`toContinuousMulEquiv_symm_apply` 📖	mathematical	`IsOpen` `Set.preimage` `DFunLike.coe` `MulEquiv` `EquivLike.toFunLike` `instEquivLike`	`ContinuousMulEquiv` `ContinuousMulEquiv.instEquivLike` `ContinuousMulEquiv.symm` `toContinuousMulEquiv` `symm`	—	—
`toHomeomorph_toContinuousMulEquiv` 📖	mathematical	`IsOpen` `Set.preimage` `DFunLike.coe` `MulEquiv` `EquivLike.toFunLike` `instEquivLike`	`HomeomorphClass.toHomeomorph` `ContinuousMulEquiv` `ContinuousMulEquiv.instEquivLike` `ContinuousMulEquiv.instHomeomorphClass` `toContinuousMulEquiv` `Equiv.toHomeomorph` `toEquiv`	—	`ContinuousMulEquiv.instHomeomorphClass`
`toMulEquiv_toContinuousMulEquiv` 📖	mathematical	`IsOpen` `Set.preimage` `DFunLike.coe` `MulEquiv` `EquivLike.toFunLike` `instEquivLike`	`MulEquivClass.toMulEquiv` `ContinuousMulEquiv` `ContinuousMulEquiv.instEquivLike` `ContinuousMulEquiv.instMulEquivClass` `toContinuousMulEquiv`	—	`ContinuousMulEquiv.instMulEquivClass`

(root)

Definitions

Name	Category	Theorems
`ContinuousAddEquiv` 📖	CompData	45 math math: `AddSubgroup.addSubgroupOfContinuousAddEquivOfLe_apply`, `ContinuousAddEquiv.eq_comp_symm`, `ContinuousAddEquiv.symm_comp_eq`, `ContinuousAddEquiv.instAddEquivClass`, `ContinuousAddEquiv.coe_refl`, `ContinuousAddEquiv.instHomeomorphClass`, `MeasureTheory.addEquivAddHaarChar_smul_preimage`, `AddEquiv.toHomeomorph_toContinuousAddEquiv`, `ContinuousAddEquiv.symm_bijective`, `MeasureTheory.addEquivAddHaarChar_eq`, `AddEquiv.toContinuousAddEquiv_apply`, `AddEquiv.toAddEquiv_toContinuousAddEquiv`, `ContinuousAddEquiv.surjective`, `MeasureTheory.integral_comap_eq_addEquivAddHaarChar_smul`, `ContinuousAddEquiv.symm_apply_eq`, `ContinuousAddEquiv.toEquiv_eq_coe`, `ContinuousAddEquiv.eq_symm_comp`, `ContinuousAddEquiv.symm_comp_self`, `ContinuousAddEquiv.self_comp_symm`, `ContinuousAddEquiv.toHomeomorph_eq_coe`, `ContinuousAddEquiv.isAddHaarMeasure_map`, `MeasureTheory.addEquivAddHaarChar_smul_map`, `ContinuousAddEquiv.apply_eq_iff_eq`, `ContinuousAddEquiv.toAddEquiv_eq_coe`, `ContinuousAddEquiv.invFun_eq_symm`, `ContinuousAddEquiv.ext_iff`, `MeasureTheory.addEquivAddHaarChar_smul_eq_comap`, `ContinuousAddEquiv.injective`, `ContinuousAddEquiv.eq_symm_apply`, `ContinuousAddEquiv.coe_mk`, `ContinuousAddEquiv.apply_eq_iff_symm_apply`, `AddSubgroup.addSubgroupOfContinuousAddEquivOfLe_symm_apply`, `ContinuousAddEquiv.symm_apply_apply`, `ContinuousAddEquiv.bijective`, `AddSubgroup.addSubgroupOfContinuousAddEquivOfLe_toAddEquiv`, `ContinuousAddEquiv.comp_symm_eq`, `ContinuousAddEquiv.refl_apply`, `ContinuousAddEquiv.equivLike_neg_eq_symm`, `AddEquiv.toContinuousAddEquiv_symm_apply`, `MeasureTheory.addEquivAddHaarChar_smul_integral_map`, `ContinuousAddEquiv.coe_trans`, `ContinuousAddEquiv.apply_symm_apply`, `ContinuousAddEquiv.trans_apply`, `ContinuousAddEquiv.coe_toHomeomorph_symm`, `ContinuousAddEquiv.symm_trans_apply`
`ContinuousAddMonoidHom` 📖	CompData	62 math math: `ContinuousAddMonoidHom.coe_id`, `ContinuousLinearMap.toContinuousAddMonoidHom_add`, `ContinuousAddMonoidHom.snd_toFun`, `ContinuousAddMonoidHom.prodMap_toFun`, `ContinuousAddMonoidHom.instAddMonoidHomClass`, `ContinuousAddMonoidHom.locallyCompactSpace_of_hasBasis`, `ProfiniteAddGrp.ofHom_apply`, `ContinuousAddMonoidHom.continuous_comp`, `ProfiniteAddGrp.instFaithfulProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap`, `ContinuousAddMonoidHom.coe_comp`, `ProfiniteAddGrp.instPreservesLimitsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap`, `ProfiniteAddGrp.hom_neg_apply`, `ContinuousAddMonoidHom.nsmul_apply`, `ProfiniteAddGrp.neg_hom_apply`, `ContinuousAddMonoidHom.inl_toFun`, `ProfiniteAddGrp.comp_apply`, `ContinuousAddMonoidHom.instContinuousEvalConst`, `ContinuousAddMonoidHom.range_toContinuousMap`, `ContinuousAddMonoidHom.toContinuousMap_toContinuousAddMonoidHom`, `lp.singleContinuousAddMonoidHom_apply`, `ContinuousLinearMap.toContinuousAddMonoidHom_zero`, `ContinuousAddMonoidHom.continuous_comp_right`, `ProfiniteAddGrp.instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap`, `ProfiniteAddGrp.id_apply`, `ContinuousAddMonoidHom.coe_toContinuousMap`, `LinearMap.IsSymmetric.toSelfAdjoint_apply`, `ProfiniteAddGrp.coe_id`, `ContinuousAddMonoidHom.toAddMonoidHom_injective`, `ContinuousAddMonoidHom.zero_toFun`, `ContinuousAddMonoidHom.ext_iff`, `ContinuousAddMonoidHom.isClosedEmbedding_toContinuousMap`, `ContinuousAddMonoidHom.prod_toFun`, `ContinuousAddMonoidHom.coprod_toFun`, `ContinuousLinearMap.toContinuousAddMonoidHom_injective`, `ContinuousAddMonoidHom.isInducing_toContinuousMap`, `ContinuousAddMonoidHom.coe_zero`, `ContinuousAddMonoidHom.toAddMonoidHom_toContinuousAddMonoidHom`, `ContinuousAddMonoidHom.instCompactSpace`, `ContinuousLinearMap.toContinuousAddMonoidHom_neg`, `ContinuousAddMonoidHom.neg_toFun`, `ContinuousAddMonoidHom.coe_coe`, `ContinuousAddMonoidHom.fst_toFun`, `ContinuousAddMonoidHom.instIsTopologicalAddGroup`, `ProfiniteAddGrp.coe_comp`, `ContinuousLinearMap.toContinuousAddMonoidHom_sub`, `ContinuousAddMonoidHom.isEmbedding_toContinuousMap`, `ContinuousAddMonoidHom.isClosedEmbedding_coe`, `SeparationQuotient.liftNormedAddGroupHom_apply`, `ContinuousAddMonoidHom.diag_toFun`, `ContinuousAddMonoidHom.instT2Space`, `ContinuousAddMonoidHom.add_toFun`, `ContinuousAddMonoidHom.add_apply`, `ContinuousAddMonoidHom.comp_toFun`, `ContinuousAddMonoidHom.inr_toFun`, `ContinuousAddMonoidHom.id_toFun`, `ContinuousAddMonoidHom.coe_toAddMonoidHom`, `ContinuousAddMonoidHom.instContinuousEval`, `ContinuousAddMonoidHom.instContinuousMapClass`, `ContinuousAddMonoidHom.toContinuousMap_injective`, `ContinuousAddMonoidHom.locallyCompactSpace_of_equicontinuousAt`, `ContinuousAddMonoidHom.swap_toFun`, `ContinuousAddMonoidHom.continuous_comp_left`
`ContinuousMonoidHom` 📖	CompData	70 math math: `ContinuousMonoidHom.toContinuousMap_toContinuousMonoidHom`, `ProfiniteGrp.instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap`, `ContinuousMonoidHom.instIsTopologicalGroup`, `PontryaginDual.map_one`, `ContinuousMonoidHom.toMonoidHom_injective`, `ContinuousMonoidHom.isInducing_toContinuousMap`, `ProfiniteGrp.ProfiniteCompletion.lift_eta`, `ContinuousMonoidHom.coe_toContinuousMap`, `ProfiniteGrp.coe_id`, `PontryaginDual.map_mul`, `ProfiniteGrp.ProfiniteCompletion.lift_eta_assoc`, `ProfiniteGrp.instFaithfulProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap`, `ProfiniteGrp.toLimit_surjective`, `ContinuousMonoidHom.swap_toFun`, `ContinuousMonoidHom.coe_id`, `ContinuousMonoidHom.snd_toFun`, `ProfiniteGrp.denseRange_toLimit`, `ProfiniteGrp.comp_apply`, `ContinuousMonoidHom.locallyCompactSpace_of_equicontinuousAt`, `ContinuousMonoidHom.mul_toFun`, `ContinuousMonoidHom.ext_iff`, `ProfiniteGrp.inv_hom_apply`, `ContinuousMonoidHom.inv_toFun`, `ContAction.resCongr_hom`, `ContinuousMonoidHom.toContinuousMap_injective`, `ContAction.res_obj_obj`, `ContinuousMonoidHom.coe_toMonoidHom`, `ContinuousMonoidHom.instContinuousMapClass`, `ContinuousMonoidHom.continuous_comp_left`, `ContinuousMonoidHom.instContinuousEvalConst`, `ContinuousMonoidHom.id_toFun`, `ProfiniteGrp.hom_inv_apply`, `ContinuousMonoidHom.instMonoidHomClass`, `ContinuousMonoidHom.coe_one`, `ContinuousMonoidHom.continuous_comp_right`, `ContinuousMonoidHom.instContinuousEval`, `ContinuousMonoidHom.isEmbedding_toContinuousMap`, `ContinuousMonoidHom.mul_apply`, `ContinuousMonoidHom.pow_apply`, `ContinuousMonoidHom.diag_toFun`, `ContinuousMonoidHom.comp_toFun`, `ProfiniteGrp.toLimit_injective`, `ContinuousMonoidHom.instT2Space`, `ProfiniteGrp.ofHom_apply`, `ContinuousMonoidHom.coe_comp`, `ContAction.resCongr_inv`, `ContinuousMonoidHom.isClosedEmbedding_toContinuousMap`, `ContinuousMonoidHom.range_toContinuousMap`, `ContinuousMonoidHom.inl_toFun`, `PontryaginDual.map_apply`, `ContinuousMonoidHom.instCompactSpace`, `ProfiniteGrp.coe_comp`, `ContinuousMonoidHom.coe_coe`, `ContinuousMonoidHom.inr_toFun`, `ContinuousMonoidHom.coprod_toFun`, `ContinuousMonoidHom.locallyCompactSpace_of_hasBasis`, `ProfiniteGrp.diagram_map`, `ContinuousMonoidHom.prod_toFun`, `ProfiniteGrp.id_apply`, `ContinuousMonoidHom.one_toFun`, `ContinuousMonoidHom.continuous_comp`, `ContinuousMonoidHom.fst_toFun`, `ProfiniteGrp.instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap`, `ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap`, `ContAction.res_map`, `ContinuousMonoidHom.prodMap_toFun`, `ContinuousMonoidHom.isClosedEmbedding_coe`, `ContinuousMonoidHom.toMonoidHom_toContinuousMonoidHom`, `ProfiniteGrp.diagram_obj`, `ProfiniteGrp.instReflectsIsomorphismsForgetContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite`
`ContinuousMulEquiv` 📖	CompData	50 math math: `MeasureTheory.mulEquivHaarChar_smul_integral_map`, `ContinuousMulEquiv.coe_refl`, `ContinuousMulEquiv.instHomeomorphClass`, `ContinuousMulEquiv.surjective`, `Subgroup.subgroupOfContinuousMulEquivOfLe_toMulEquiv`, `MulEquiv.toContinuousMulEquiv_symm_apply`, `ContinuousMulEquiv.coe_trans`, `MulEquiv.toMulEquiv_toContinuousMulEquiv`, `MeasureTheory.mulEquivHaarChar_eq`, `ContinuousMulEquiv.eq_comp_symm`, `ContinuousMulEquiv.symm_apply_eq`, `ContinuousMulEquiv.symm_comp_self`, `ContinuousMulEquiv.eq_symm_apply`, `ContinuousMulEquiv.symm_bijective`, `ContAction.resEquiv_inverse`, `MulEquiv.toContinuousMulEquiv_apply`, `ContinuousMulEquiv.eq_symm_comp`, `MeasureTheory.mulEquivHaarChar_smul_map`, `ContinuousMulEquiv.symm_trans_apply`, `ContinuousMulEquiv.invFun_eq_symm`, `ContinuousMulEquiv.coe_mk'`, `MulEquiv.toHomeomorph_toContinuousMulEquiv`, `ContinuousMulEquiv.symm_apply_apply`, `ContinuousMulEquiv.apply_symm_apply`, `ContinuousMulEquiv.toMulEquiv_eq_coe`, `ContAction.resEquiv_functor`, `ContinuousMulEquiv.coe_mk`, `Subgroup.subgroupOfContinuousMulEquivOfLe_apply`, `ContinuousMulEquiv.self_comp_symm`, `ContinuousMulEquiv.instMulEquivClass`, `ContinuousMulEquiv.apply_eq_iff_eq`, `ContinuousMulEquiv.ext_iff`, `ContinuousMulEquiv.isHaarMeasure_map`, `Units.toMulEquiv_mapContinuousMulEquiv`, `MeasureTheory.mulEquivHaarChar_smul_preimage`, `Subgroup.subgroupOfContinuousMulEquivOfLe_symm_apply`, `ContinuousMulEquiv.injective`, `ContinuousMulEquiv.trans_apply`, `MeasureTheory.mulEquivHaarChar_smul_eq_comap`, `ContinuousMulEquiv.refl_apply`, `ContinuousMulEquiv.equivLike_inv_eq_symm`, `ContinuousMulEquiv.symm_comp_eq`, `ContinuousMulEquiv.coe_toHomeomorph_symm`, `ContinuousMulEquiv.toEquiv_eq_coe`, `ContinuousMulEquiv.toHomeomorph_eq_coe`, `ContinuousMulEquiv.bijective`, `ContinuousMulEquiv.apply_eq_iff_symm_apply`, `Units.mapContinuousMulEquiv_apply`, `MeasureTheory.integral_comap_eq_mulEquivHaarChar_smul`, `ContinuousMulEquiv.comp_symm_eq`
`«term_≃ₜ*_»` 📖	CompOp	—
`«term_≃ₜ+_»` 📖	CompOp	—

---

← Back to Index