CompactOpen

📁 Source: Mathlib/Topology/Algebra/Group/CompactOpen.lean

Statistics

Metric	Count
Definitions compLeft, compRight, instTopologicalSpace, compLeft, compRight, instTopologicalSpace	6
Theorems continuous_comp, continuous_comp_left, continuous_comp_right, continuous_of_continuous_uncurry, instCompactSpace, instContinuousEval, instContinuousEvalConst, instIsTopologicalAddGroup, instT2Space, isClosedEmbedding_coe, isClosedEmbedding_toContinuousMap, isEmbedding_toContinuousMap, isInducing_toContinuousMap, locallyCompactSpace_of_equicontinuousAt, locallyCompactSpace_of_hasBasis, range_toContinuousMap, continuous_comp, continuous_comp_left, continuous_comp_right, continuous_of_continuous_uncurry, instCompactSpace, instContinuousEval, instContinuousEvalConst, instIsTopologicalGroup, instT2Space, isClosedEmbedding_coe, isClosedEmbedding_toContinuousMap, isEmbedding_toContinuousMap, isInducing_toContinuousMap, locallyCompactSpace_of_equicontinuousAt, locallyCompactSpace_of_hasBasis, range_toContinuousMap	32
Total	38

ContinuousAddMonoidHom

Definitions

Name	Category	Theorems
compLeft 📖	CompOp	—
compRight 📖	CompOp	—
instTopologicalSpace 📖	CompOp	15 math math: locallyCompactSpace_of_hasBasis, continuous_comp, instContinuousEvalConst, continuous_comp_right, isClosedEmbedding_toContinuousMap, continuous_of_continuous_uncurry, isInducing_toContinuousMap, instCompactSpace, instIsTopologicalAddGroup, isEmbedding_toContinuousMap, isClosedEmbedding_coe, instT2Space, instContinuousEval, locallyCompactSpace_of_equicontinuousAt, continuous_comp_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_comp 📖	mathematical	—	Continuous ContinuousAddMonoidHom instTopologicalSpaceProd instTopologicalSpace comp	—	Topology.IsInducing.continuous_iff isInducing_toContinuousMap Continuous.comp ContinuousMap.continuous_comp' instLocallyCompactPairOfLocallyCompactSpace Topology.IsInducing.continuous Topology.IsInducing.prodMap
continuous_comp_left 📖	mathematical	—	Continuous ContinuousAddMonoidHom instTopologicalSpace comp	—	Topology.IsInducing.continuous_iff isInducing_toContinuousMap Continuous.comp ContinuousMap.continuous_precomp Topology.IsInducing.continuous
continuous_comp_right 📖	mathematical	—	Continuous ContinuousAddMonoidHom instTopologicalSpace comp	—	Topology.IsInducing.continuous_iff isInducing_toContinuousMap Continuous.comp ContinuousMap.continuous_postcomp Topology.IsInducing.continuous
continuous_of_continuous_uncurry 📖	mathematical	Continuous instTopologicalSpaceProd DFunLike.coe ContinuousAddMonoidHom instFunLike	instTopologicalSpace	—	Topology.IsInducing.continuous_iff isInducing_toContinuousMap ContinuousMap.continuous_of_continuous_uncurry
instCompactSpace 📖	mathematical	—	CompactSpace ContinuousAddMonoidHom instTopologicalSpace	—	Topology.IsClosedEmbedding.compactSpace Function.compactSpace isClosedEmbedding_coe
instContinuousEval 📖	mathematical	—	ContinuousEval ContinuousAddMonoidHom instFunLike instTopologicalSpace	—	ContinuousEval.of_continuous_forget ContinuousMap.instContinuousEvalOfLocallyCompactPair Topology.IsInducing.continuous isInducing_toContinuousMap
instContinuousEvalConst 📖	mathematical	—	ContinuousEvalConst ContinuousAddMonoidHom instFunLike instTopologicalSpace	—	ContinuousEvalConst.of_continuous_forget ContinuousMap.instContinuousEvalConst Topology.IsInducing.continuous isInducing_toContinuousMap
instIsTopologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup ContinuousAddMonoidHom SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instTopologicalSpace instAddCommGroup	—	isInducing_toContinuousMap Topology.IsInducing.continuous Topology.IsInducing.continuous_iff Continuous.comp IsTopologicalAddGroup.toContinuousAdd continuous_add ContinuousMap.instIsTopologicalAddGroup Continuous.prodMap IsTopologicalAddGroup.toContinuousNeg ContinuousNeg.continuous_neg
instT2Space 📖	mathematical	—	T2Space ContinuousAddMonoidHom instTopologicalSpace	—	Topology.IsEmbedding.t2Space ContinuousMap.instT2Space isEmbedding_toContinuousMap
isClosedEmbedding_coe 📖	mathematical	—	Topology.IsClosedEmbedding ContinuousAddMonoidHom instTopologicalSpace Pi.topologicalSpace DFunLike.coe instFunLike	—	Topology.IsClosedEmbedding.comp IsHomeomorph.isClosedEmbedding ContinuousMap.isHomeomorph_coe isClosedEmbedding_toContinuousMap
isClosedEmbedding_toContinuousMap 📖	mathematical	—	Topology.IsClosedEmbedding ContinuousAddMonoidHom ContinuousMap instTopologicalSpace ContinuousMap.compactOpen toContinuousMap	—	isEmbedding_toContinuousMap range_toContinuousMap Set.setOf_forall IsClosed.inter IsClosed.preimage ContinuousEvalConst.continuous_eval_const ContinuousMap.instContinuousEvalConst isClosed_singleton T2Space.t1Space isClosed_iInter isClosed_eq Continuous.add
isEmbedding_toContinuousMap 📖	mathematical	—	Topology.IsEmbedding ContinuousAddMonoidHom ContinuousMap instTopologicalSpace ContinuousMap.compactOpen toContinuousMap	—	isInducing_toContinuousMap toContinuousMap_injective
isInducing_toContinuousMap 📖	mathematical	—	Topology.IsInducing ContinuousAddMonoidHom ContinuousMap instTopologicalSpace ContinuousMap.compactOpen toContinuousMap	—	—
locallyCompactSpace_of_equicontinuousAt 📖	mathematical	IsCompact Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid EquicontinuousAt Set.Elem AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup setOf Set.MapsTo DFunLike.coe AddMonoidHom.instFunLike Set.instMembership AddGroup.toSubtractionMonoid	LocallyCompactSpace ContinuousAddMonoidHom instTopologicalSpace	—	equicontinuous_of_equicontinuousAt_zero AddMonoidHom.instAddMonoidHomClass local_compact_nhds WeaklyLocallyCompactSpace.locallyCompactSpace instR1Space IsTopologicalAddGroup.regularSpace IsUniformAddGroup.to_topologicalAddGroup instWeaklyLocallyCompactSpaceOfCompactSpace instContinuousMapClass Equicontinuous.comp Set.MapsTo.mono_right Set.ext instAddMonoidHomClass Equicontinuous.continuous equicontinuous_iff_range Set.image_eq_range Set.ext_iff Set.mem_image IsClosed.inter isClosed_set_pi IsCompact.isClosed T25Space.t2Space T3Space.t25Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace instT1SpaceOfT0SpaceOfR0Space instR0Space NormalSpace.of_regularSpace_lindelofSpace instLindelofSpaceOfSigmaCompactSpace CompactSpace.sigmaCompact AddMonoidHom.isClosed_range_coe IsTopologicalAddGroup.toContinuousAdd mem_interior_iff_mem_nhds interior_subset isOpen_induced ContinuousMap.isOpen_setOf_mapsTo isOpen_interior Set.Nonempty.mono interior_maximal TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_addGroup instIsTopologicalAddGroup Topology.IsInducing.isCompact_iff isInducing_toContinuousMap ArzelaAscoli.isCompact_of_equicontinuous IsClosed.isCompact Function.compactSpace
locallyCompactSpace_of_hasBasis 📖	mathematical	Set Set.instMembership Filter.HasBasis nhds UniformSpace.toTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	LocallyCompactSpace ContinuousAddMonoidHom SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instTopologicalSpace	—	WeaklyLocallyCompactSpace.exists_compact_mem_nhds instWeaklyLocallyCompactSpaceOfLocallyCompactSpace exists_closed_nhds_zero_neg_eq_add_subset Set.add_mem_add mem_of_mem_nhds add_zero map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass locallyCompactSpace_of_equicontinuousAt Filter.HasBasis.mem_of_mem Filter.HasBasis.equicontinuousAt_iff_right Filter.HasBasis.uniformity_of_nhds_zero Filter.eventually_iff_exists_mem Set.mem_setOf_eq map_zero AddMonoidHomClass.toZeroHomClass sub_zero
range_toContinuousMap 📖	mathematical	—	Set.range ContinuousMap ContinuousAddMonoidHom toContinuousMap setOf DFunLike.coe ContinuousMap.instFunLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	Set.Subset.antisymm Set.range_subset_iff map_zero AddMonoidHomClass.toZeroHomClass instAddMonoidHomClass map_add AddMonoidHomClass.toAddHomClass ContinuousMap.continuous_toFun

ContinuousMonoidHom

Definitions

Name	Category	Theorems
compLeft 📖	CompOp	—
compRight 📖	CompOp	—
instTopologicalSpace 📖	CompOp	15 math math: instIsTopologicalGroup, isInducing_toContinuousMap, locallyCompactSpace_of_equicontinuousAt, continuous_comp_left, instContinuousEvalConst, continuous_comp_right, instContinuousEval, isEmbedding_toContinuousMap, continuous_of_continuous_uncurry, instT2Space, isClosedEmbedding_toContinuousMap, instCompactSpace, locallyCompactSpace_of_hasBasis, continuous_comp, isClosedEmbedding_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_comp 📖	mathematical	—	Continuous ContinuousMonoidHom instTopologicalSpaceProd instTopologicalSpace comp	—	Topology.IsInducing.continuous_iff isInducing_toContinuousMap Continuous.comp ContinuousMap.continuous_comp' instLocallyCompactPairOfLocallyCompactSpace Topology.IsInducing.continuous Topology.IsInducing.prodMap
continuous_comp_left 📖	mathematical	—	Continuous ContinuousMonoidHom instTopologicalSpace comp	—	Topology.IsInducing.continuous_iff isInducing_toContinuousMap Continuous.comp ContinuousMap.continuous_precomp Topology.IsInducing.continuous
continuous_comp_right 📖	mathematical	—	Continuous ContinuousMonoidHom instTopologicalSpace comp	—	Topology.IsInducing.continuous_iff isInducing_toContinuousMap Continuous.comp ContinuousMap.continuous_postcomp Topology.IsInducing.continuous
continuous_of_continuous_uncurry 📖	mathematical	Continuous instTopologicalSpaceProd DFunLike.coe ContinuousMonoidHom instFunLike	instTopologicalSpace	—	Topology.IsInducing.continuous_iff isInducing_toContinuousMap ContinuousMap.continuous_of_continuous_uncurry
instCompactSpace 📖	mathematical	—	CompactSpace ContinuousMonoidHom instTopologicalSpace	—	Topology.IsClosedEmbedding.compactSpace Function.compactSpace isClosedEmbedding_coe
instContinuousEval 📖	mathematical	—	ContinuousEval ContinuousMonoidHom instFunLike instTopologicalSpace	—	ContinuousEval.of_continuous_forget ContinuousMap.instContinuousEvalOfLocallyCompactPair Topology.IsInducing.continuous isInducing_toContinuousMap
instContinuousEvalConst 📖	mathematical	—	ContinuousEvalConst ContinuousMonoidHom instFunLike instTopologicalSpace	—	ContinuousEvalConst.of_continuous_forget ContinuousMap.instContinuousEvalConst Topology.IsInducing.continuous isInducing_toContinuousMap
instIsTopologicalGroup 📖	mathematical	—	IsTopologicalGroup ContinuousMonoidHom DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instTopologicalSpace instCommGroup	—	isInducing_toContinuousMap Topology.IsInducing.continuous Topology.IsInducing.continuous_iff Continuous.comp IsTopologicalGroup.toContinuousMul continuous_mul ContinuousMap.instIsTopologicalGroup Continuous.prodMap IsTopologicalGroup.toContinuousInv ContinuousInv.continuous_inv
instT2Space 📖	mathematical	—	T2Space ContinuousMonoidHom instTopologicalSpace	—	Topology.IsEmbedding.t2Space ContinuousMap.instT2Space isEmbedding_toContinuousMap
isClosedEmbedding_coe 📖	mathematical	—	Topology.IsClosedEmbedding ContinuousMonoidHom instTopologicalSpace Pi.topologicalSpace DFunLike.coe instFunLike	—	Topology.IsClosedEmbedding.comp IsHomeomorph.isClosedEmbedding ContinuousMap.isHomeomorph_coe isClosedEmbedding_toContinuousMap
isClosedEmbedding_toContinuousMap 📖	mathematical	—	Topology.IsClosedEmbedding ContinuousMonoidHom ContinuousMap instTopologicalSpace ContinuousMap.compactOpen toContinuousMap	—	isEmbedding_toContinuousMap range_toContinuousMap Set.setOf_forall IsClosed.inter IsClosed.preimage ContinuousEvalConst.continuous_eval_const ContinuousMap.instContinuousEvalConst isClosed_singleton T2Space.t1Space isClosed_iInter isClosed_eq Continuous.mul
isEmbedding_toContinuousMap 📖	mathematical	—	Topology.IsEmbedding ContinuousMonoidHom ContinuousMap instTopologicalSpace ContinuousMap.compactOpen toContinuousMap	—	isInducing_toContinuousMap toContinuousMap_injective
isInducing_toContinuousMap 📖	mathematical	—	Topology.IsInducing ContinuousMonoidHom ContinuousMap instTopologicalSpace ContinuousMap.compactOpen toContinuousMap	—	—
locallyCompactSpace_of_equicontinuousAt 📖	mathematical	IsCompact Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid EquicontinuousAt Set.Elem MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup setOf Set.MapsTo DFunLike.coe MonoidHom.instFunLike Set.instMembership Group.toDivisionMonoid	LocallyCompactSpace ContinuousMonoidHom instTopologicalSpace	—	equicontinuous_of_equicontinuousAt_one MonoidHom.instMonoidHomClass local_compact_nhds WeaklyLocallyCompactSpace.locallyCompactSpace instR1Space IsTopologicalGroup.regularSpace IsUniformGroup.to_topologicalGroup instWeaklyLocallyCompactSpaceOfCompactSpace instContinuousMapClass Equicontinuous.comp Set.MapsTo.mono_right Set.ext instMonoidHomClass Equicontinuous.continuous equicontinuous_iff_range Set.image_eq_range IsClosed.inter isClosed_set_pi IsCompact.isClosed T25Space.t2Space T3Space.t25Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace instT1SpaceOfT0SpaceOfR0Space instR0Space NormalSpace.of_regularSpace_lindelofSpace instLindelofSpaceOfSigmaCompactSpace CompactSpace.sigmaCompact MonoidHom.isClosed_range_coe IsTopologicalGroup.toContinuousMul mem_interior_iff_mem_nhds interior_subset isOpen_induced ContinuousMap.isOpen_setOf_mapsTo isOpen_interior Set.Nonempty.mono interior_maximal TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group instIsTopologicalGroup Topology.IsInducing.isCompact_iff isInducing_toContinuousMap ArzelaAscoli.isCompact_of_equicontinuous IsClosed.isCompact Function.compactSpace
locallyCompactSpace_of_hasBasis 📖	mathematical	Set Set.instMembership Filter.HasBasis nhds UniformSpace.toTopologicalSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	LocallyCompactSpace ContinuousMonoidHom DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instTopologicalSpace	—	WeaklyLocallyCompactSpace.exists_compact_mem_nhds instWeaklyLocallyCompactSpaceOfLocallyCompactSpace exists_closed_nhds_one_inv_eq_mul_subset Set.mul_mem_mul mem_of_mem_nhds mul_one map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass locallyCompactSpace_of_equicontinuousAt Filter.HasBasis.mem_of_mem Filter.HasBasis.equicontinuousAt_iff_right Filter.HasBasis.uniformity_of_nhds_one Filter.eventually_iff_exists_mem Set.mem_setOf_eq map_one MonoidHomClass.toOneHomClass div_one
range_toContinuousMap 📖	mathematical	—	Set.range ContinuousMap ContinuousMonoidHom toContinuousMap setOf DFunLike.coe ContinuousMap.instFunLike MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	Set.Subset.antisymm Set.range_subset_iff map_one MonoidHomClass.toOneHomClass instMonoidHomClass map_mul MonoidHomClass.toMulHomClass ContinuousMap.continuous_toFun

---

← Back to Index