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	Continuous ContinuousAddMonoidHom 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 SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup UniformSpace.toTopologicalSpace 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 UniformSpace.toTopologicalSpace 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	Continuous ContinuousMonoidHom 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 DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup UniformSpace.toTopologicalSpace 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 UniformSpace.toTopologicalSpace 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