Basic

📁 Source: Mathlib/Topology/Compactification/OnePoint/Basic.lean

Statistics

Metric	Count
Definitions onePointCongr, OnePoint, continuousMapDiscreteEquiv, continuousMapMk, continuousMapMkDiscrete, continuousMapMkNat, continuousMapNatEquiv, elim, equivOfIsEmbeddingOfRangeEq, infty, instCoeTC, instFintype, instInhabited, instTopologicalSpace, map, opensOfCompl, rec, some, «term∞», instReprOnePoint	20
Theorems t1_counterexample, onePointCongr_apply, onePointCongr_symm_apply, canLift, coe_eq_coe, coe_injective, coe_ne_infty, coe_preimage_infty, comap_coe_nhds, comap_coe_nhds_infty, compl_image_coe, compl_infty, compl_range_coe, continuousAt_coe, continuousAt_infty, continuousAt_infty', continuous_coe, continuous_iff, continuous_iff_from_discrete, continuous_iff_from_nat, continuous_map, continuous_map_iff, denseRange_coe, elim_infty, elim_some, equivOfIsEmbeddingOfRangeEq_apply_coe, equivOfIsEmbeddingOfRangeEq_apply_infty, exists, forall, hasBasis_nhds_infty, infinite, infty_mem_opensOfCompl, infty_ne_coe, infty_notMem_image_coe, infty_notMem_range_coe, inseparable_coe, inseparable_iff, insert_infty_range_coe, instCompactSpace, instConnectedSpaceOfPreconnectedSpaceOfNoncompactSpace, instNormalSpaceOfWeaklyLocallyCompactSpaceOfR1Space, instT0Space, instT1Space, instTotallySeparatedSpaceOfDiscreteTopology, isClosed_iff_of_mem, isClosed_iff_of_notMem, isClosed_image_coe, isClosed_infty, isCompl_range_coe_infty, isDenseEmbedding_coe, isOpenEmbedding_coe, isOpenMap_coe, isOpen_compl_image_coe, isOpen_def, isOpen_iff_of_mem, isOpen_iff_of_mem', isOpen_iff_of_notMem, isOpen_image_coe, isOpen_range_coe, le_nhds_infty, map_comp, map_id, map_infty, map_some, ne_infty_iff_exists, nhdsNE_coe_neBot, nhdsNE_infty_eq, nhdsNE_infty_neBot, nhdsNE_neBot, nhdsWithin_coe, nhdsWithin_coe_image, nhds_coe_eq, nhds_infty_eq, notMem_range_coe_iff, not_continuous_cofiniteTopology_of_symm, not_inseparable_coe_infty, not_inseparable_infty_coe, not_specializes_infty_coe, range_coe_inter_infty, range_coe_union_infty, some_eq_iff, specializes_coe, tendsto_coe_infty, tendsto_nhds_infty, tendsto_nhds_infty', ultrafilter_le_nhds_infty	86
Total	106

Continuous.homeoOfEquivCompactToT2

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
t1_counterexample 📖	mathematical	—	CompactSpace T1Space Continuous DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	OnePoint.instCompactSpace instT1SpaceCofiniteTopology CofiniteTopology.continuous_of OnePoint.instT1Space T2Space.t1Space DiscreteTopology.toT2Space instDiscreteTopologyNat OnePoint.not_continuous_cofiniteTopology_of_symm instInfiniteNat

Homeomorph

Definitions

Name	Category	Theorems
onePointCongr 📖	CompOp	2 math math: onePointCongr_symm_apply, onePointCongr_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
onePointCongr_apply 📖	mathematical	—	DFunLike.coe Homeomorph OnePoint OnePoint.instTopologicalSpace EquivLike.toFunLike instEquivLike onePointCongr OnePoint.map	—	—
onePointCongr_symm_apply 📖	mathematical	—	DFunLike.coe Homeomorph OnePoint OnePoint.instTopologicalSpace EquivLike.toFunLike instEquivLike symm onePointCongr OnePoint.map	—	—

OnePoint

Definitions

Name	Category	Theorems
continuousMapDiscreteEquiv 📖	CompOp	—
continuousMapMk 📖	CompOp	—
continuousMapMkDiscrete 📖	CompOp	—
continuousMapMkNat 📖	CompOp	—
continuousMapNatEquiv 📖	CompOp	—
elim 📖	CompOp	2 math math: elim_some, elim_infty
equivOfIsEmbeddingOfRangeEq 📖	CompOp	2 math math: equivOfIsEmbeddingOfRangeEq_apply_infty, equivOfIsEmbeddingOfRangeEq_apply_coe
infty 📖	CompOp	57 math math: not_inseparable_infty_coe, exists, continuous_iff, isBoundedAt_iff_exists_SL2Z, equivOfIsEmbeddingOfRangeEq_apply_infty, continuousAt_infty, smul_infty_eq_self_iff, compl_infty, isClosed_infty, isZeroAt_iff_exists_SL2Z, infty_mem_opensOfCompl, notMem_range_coe_iff, nhdsNE_infty_neBot, infty_notMem_image_coe, isCusp_SL2Z_iff', tendsto_nhds_infty, smul_some_eq_ite, coe_preimage_infty, compl_range_coe, LightProfinite.continuous_iff_convergent, isZeroAt_infty_iff, canLift, isBoundedAt_infty_iff, elim_infty, instFactIsCuspInftyRealOfIsArithmetic, equivProjectivization_symm_apply_mk, not_specializes_infty_coe, comap_coe_nhds_infty, smul_infty_eq_ite, Rat.not_countably_generated_nhds_infty_opc, compl_image_coe, nhdsNE_infty_eq, continuous_iff_from_discrete, hasBasis_nhds_infty, smul_infty_def, continuousAt_infty', cosetToCuspOrbit_apply_mk, exists_mem_SL2, range_coe_union_infty, inseparable_iff, range_coe_inter_infty, Subgroup.strictWidthInfty_pos_iff, map_infty, Subgroup.isCusp_of_mem_strictPeriods, nhds_infty_eq, infty_notMem_range_coe, insert_infty_range_coe, ultrafilter_le_nhds_infty, Subgroup.widthInfty_pos_iff, tendsto_nhds_infty', tendsto_coe_infty, forall, not_inseparable_coe_infty, le_nhds_infty, continuous_iff_from_nat, isCompl_range_coe_infty, equivProjectivization_apply_infinity
instCoeTC 📖	CompOp	—
instFintype 📖	CompOp	—
instInhabited 📖	CompOp	—
instTopologicalSpace 📖	CompOp	64 math math: not_inseparable_infty_coe, isOpen_def, instConnectedSpaceOfPreconnectedSpaceOfNoncompactSpace, continuous_iff, nhdsWithin_coe, nhdsWithin_coe_image, isClosed_iff_of_notMem, denseRange_coe, equivOfIsEmbeddingOfRangeEq_apply_infty, continuousAt_infty, isOpen_iff_of_mem, equivOfIsEmbeddingOfRangeEq_apply_coe, isOpen_iff_of_mem', isClosed_infty, infty_mem_opensOfCompl, isOpen_range_coe, isOpenMap_coe, nhdsNE_infty_neBot, continuous_map, comap_coe_nhds, tendsto_nhds_infty, Rat.not_firstCountableTopology_opc, nhdsNE_neBot, LightProfinite.continuous_iff_convergent, isClosed_iff_of_mem, isClosed_image_coe, instCompactSpace, LightProfinite.instMetrizableSpaceOnePointNat, instNormalSpaceOfWeaklyLocallyCompactSpaceOfR1Space, nhds_coe_eq, isOpen_iff_of_notMem, Homeomorph.onePointCongr_symm_apply, not_specializes_infty_coe, isOpenEmbedding_coe, inseparable_coe, comap_coe_nhds_infty, instT0Space, Rat.not_countably_generated_nhds_infty_opc, Rat.not_secondCountableTopology_opc, Homeomorph.onePointCongr_apply, nhdsNE_infty_eq, continuous_iff_from_discrete, hasBasis_nhds_infty, continuousAt_infty', inseparable_iff, not_continuous_cofiniteTopology_of_symm, isDenseEmbedding_coe, specializes_coe, continuous_map_iff, nhdsNE_coe_neBot, instTotallySeparatedSpaceOfDiscreteTopology, continuous_coe, nhds_infty_eq, ultrafilter_le_nhds_infty, tendsto_nhds_infty', tendsto_coe_infty, continuousAt_coe, not_inseparable_coe_infty, isOpen_compl_image_coe, le_nhds_infty, instT1Space, continuous_iff_from_nat, LightProfinite.isClosedEmbedding_natUnionInftyEmbedding, isOpen_image_coe
map 📖	CompOp	11 math math: continuous_map, map_smul, map_id, Homeomorph.onePointCongr_symm_apply, isCusp_SL2Z_iff, map_comp, map_some, Homeomorph.onePointCongr_apply, cosetToCuspOrbit_apply_mk, continuous_map_iff, map_infty
opensOfCompl 📖	CompOp	1 math math: infty_mem_opensOfCompl
rec 📖	CompOp	—
some 📖	CompOp	68 math math: not_inseparable_infty_coe, isOpen_def, exists, continuous_iff, nhdsWithin_coe, nhdsWithin_coe_image, isClosed_iff_of_notMem, denseRange_coe, continuousAt_infty, isOpen_iff_of_mem, equivOfIsEmbeddingOfRangeEq_apply_coe, isOpen_iff_of_mem', compl_infty, isOpen_range_coe, notMem_range_coe_iff, isOpenMap_coe, some_eq_iff, comap_coe_nhds, infty_notMem_image_coe, coe_injective, tendsto_nhds_infty, smul_some_eq_ite, coe_preimage_infty, compl_range_coe, LightProfinite.continuous_iff_convergent, isClosed_iff_of_mem, isClosed_image_coe, elim_some, canLift, nhds_coe_eq, isOpen_iff_of_notMem, Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff, equivProjectivization_symm_apply_mk, not_specializes_infty_coe, isOpenEmbedding_coe, inseparable_coe, comap_coe_nhds_infty, map_some, smul_infty_eq_ite, compl_image_coe, nhdsNE_infty_eq, continuous_iff_from_discrete, hasBasis_nhds_infty, continuousAt_infty', range_coe_union_infty, inseparable_iff, coe_eq_coe, isDenseEmbedding_coe, specializes_coe, nhdsNE_coe_neBot, range_coe_inter_infty, continuous_coe, nhds_infty_eq, infty_notMem_range_coe, insert_infty_range_coe, ultrafilter_le_nhds_infty, tendsto_nhds_infty', tendsto_coe_infty, continuousAt_coe, equivProjectivization_apply_coe, forall, not_inseparable_coe_infty, isOpen_compl_image_coe, le_nhds_infty, continuous_iff_from_nat, isCompl_range_coe_infty, isOpen_image_coe, ne_infty_iff_exists
«term∞» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
canLift 📖	mathematical	—	CanLift OnePoint some infty	—	WithTop.canLift
coe_eq_coe 📖	mathematical	—	some	—	coe_injective
coe_injective 📖	mathematical	—	OnePoint some	—	Option.some_injective
coe_ne_infty 📖	—	—	—	—	—
coe_preimage_infty 📖	mathematical	—	Set.preimage OnePoint some Set Set.instSingletonSet infty Set.instEmptyCollection	—	Set.ext
comap_coe_nhds 📖	mathematical	—	Filter.comap OnePoint some nhds instTopologicalSpace	—	Topology.IsInducing.nhds_eq_comap Topology.IsOpenEmbedding.isInducing isOpenEmbedding_coe
comap_coe_nhds_infty 📖	mathematical	—	Filter.comap OnePoint some nhds instTopologicalSpace infty Filter.coclosedCompact	—	nhds_infty_eq Filter.comap_sup Filter.comap_map coe_injective Filter.comap_pure coe_preimage_infty Filter.principal_empty sup_of_le_left
compl_image_coe 📖	mathematical	—	Compl.compl Set OnePoint Set.instCompl Set.image some Set.instUnion Set.instSingletonSet infty	—	Function.Injective.compl_image_eq coe_injective compl_range_coe
compl_infty 📖	mathematical	—	Compl.compl Set OnePoint Set.instCompl Set.instSingletonSet infty Set.range some	—	IsCompl.compl_eq IsCompl.symm isCompl_range_coe_infty
compl_range_coe 📖	mathematical	—	Compl.compl Set OnePoint Set.instCompl Set.range some Set.instSingletonSet infty	—	Set.compl_range_some
continuousAt_coe 📖	mathematical	—	ContinuousAt OnePoint instTopologicalSpace some	—	ContinuousAt.eq_1 nhds_coe_eq Filter.tendsto_map'_iff
continuousAt_infty 📖	mathematical	—	ContinuousAt OnePoint instTopologicalSpace infty IsClosed IsCompact Set.MapsTo some Compl.compl Set Set.instCompl	—	continuousAt_infty' Filter.HasBasis.tendsto_left_iff Filter.hasBasis_coclosedCompact
continuousAt_infty' 📖	mathematical	—	ContinuousAt OnePoint instTopologicalSpace infty Filter.Tendsto some Filter.coclosedCompact nhds	—	tendsto_nhds_infty' tendsto_pure_nhds
continuous_coe 📖	mathematical	—	Continuous OnePoint instTopologicalSpace some	—	continuous_def
continuous_iff 📖	mathematical	—	Continuous OnePoint instTopologicalSpace Filter.Tendsto some Filter.coclosedCompact nhds infty	—	—
continuous_iff_from_discrete 📖	mathematical	—	Continuous OnePoint instTopologicalSpace Filter.Tendsto some Filter.cofinite nhds infty	—	Filter.coclosedCompact_eq_cocompact T2Space.r1Space DiscreteTopology.toT2Space Filter.cocompact_eq_cofinite
continuous_iff_from_nat 📖	mathematical	—	Continuous OnePoint instTopologicalSpace instTopologicalSpaceNat Filter.Tendsto some Filter.atTop Nat.instPreorder nhds infty	—	continuous_iff_from_discrete instDiscreteTopologyNat Nat.cofinite_eq_atTop
continuous_map 📖	mathematical	Continuous Filter.Tendsto Filter.coclosedCompact	OnePoint instTopologicalSpace map	—	continuous_map_iff
continuous_map_iff 📖	mathematical	—	Continuous OnePoint instTopologicalSpace map Filter.Tendsto Filter.coclosedCompact	—	Topology.IsInducing.continuous_iff Topology.IsOpenEmbedding.isInducing isOpenEmbedding_coe
denseRange_coe 📖	mathematical	—	DenseRange OnePoint instTopologicalSpace some	—	DenseRange.eq_1 compl_infty dense_compl_singleton nhdsNE_infty_neBot
elim_infty 📖	mathematical	—	elim infty	—	—
elim_some 📖	mathematical	—	elim some	—	—
equivOfIsEmbeddingOfRangeEq_apply_coe 📖	mathematical	Topology.IsEmbedding Set.range Compl.compl Set Set.instCompl Set.instSingletonSet	DFunLike.coe Homeomorph OnePoint instTopologicalSpace EquivLike.toFunLike Homeomorph.instEquivLike equivOfIsEmbeddingOfRangeEq some	—	—
equivOfIsEmbeddingOfRangeEq_apply_infty 📖	mathematical	Topology.IsEmbedding Set.range Compl.compl Set Set.instCompl Set.instSingletonSet	DFunLike.coe Homeomorph OnePoint instTopologicalSpace EquivLike.toFunLike Homeomorph.instEquivLike equivOfIsEmbeddingOfRangeEq infty	—	—
exists 📖	mathematical	—	infty some	—	—
forall 📖	mathematical	—	infty some	—	—
hasBasis_nhds_infty 📖	mathematical	—	Filter.HasBasis OnePoint Set nhds instTopologicalSpace infty IsClosed IsCompact Set.instUnion Set.image some Compl.compl Set.instCompl Set.instSingletonSet	—	nhds_infty_eq Filter.HasBasis.sup_pure Filter.HasBasis.map Filter.hasBasis_coclosedCompact
infinite 📖	mathematical	—	Infinite OnePoint	—	instInfiniteOption
infty_mem_opensOfCompl 📖	mathematical	IsCompact	OnePoint TopologicalSpace.Opens instTopologicalSpace SetLike.instMembership TopologicalSpace.Opens.instSetLike opensOfCompl infty	—	Set.mem_compl infty_notMem_image_coe
infty_ne_coe 📖	—	—	—	—	—
infty_notMem_image_coe 📖	mathematical	—	OnePoint Set Set.instMembership Set.image some infty	—	Set.notMem_subset Set.image_subset_range infty_notMem_range_coe
infty_notMem_range_coe 📖	mathematical	—	OnePoint Set Set.instMembership Set.range some infty	—	notMem_range_coe_iff
inseparable_coe 📖	mathematical	—	Inseparable OnePoint instTopologicalSpace some	—	Topology.IsInducing.inseparable_iff Topology.IsOpenEmbedding.isInducing isOpenEmbedding_coe
inseparable_iff 📖	mathematical	—	Inseparable OnePoint instTopologicalSpace infty some	—	—
insert_infty_range_coe 📖	mathematical	—	OnePoint Set Set.instInsert infty Set.range some Set.univ	—	Set.insert_none_range_some
instCompactSpace 📖	mathematical	—	CompactSpace OnePoint instTopologicalSpace	—	nhds_infty_eq Filter.Tendsto.mono_right Filter.Tendsto.mono_left Filter.tendsto_map Filter.cocompact_le_coclosedCompact le_sup_left Set.insert_none_range_some Filter.Tendsto.isCompact_insert_range_of_cocompact continuous_coe
instConnectedSpaceOfPreconnectedSpaceOfNoncompactSpace 📖	mathematical	—	ConnectedSpace OnePoint instTopologicalSpace	—	IsDenseInducing.preconnectedSpace IsDenseEmbedding.isDenseInducing isDenseEmbedding_coe
instNormalSpaceOfWeaklyLocallyCompactSpaceOfR1Space 📖	mathematical	—	NormalSpace OnePoint instTopologicalSpace	—	nhds_infty_eq disjoint_sup_right nhds_coe_eq Filter.coclosedCompact_eq_cocompact Filter.disjoint_map coe_injective Filter.principal_singleton Filter.disjoint_principal_right compl_infty disjoint_nhds_cocompact Filter.range_mem_map le_rfl Disjoint.symm specializes_coe R1Space.specializes_or_disjoint_nhds NormalSpace.of_regularSpace_lindelofSpace instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space instWeaklyLocallyCompactSpaceOfCompactSpace instCompactSpace instLindelofSpaceOfSigmaCompactSpace CompactSpace.sigmaCompact
instT0Space 📖	mathematical	—	T0Space OnePoint instTopologicalSpace	—	inseparable_iff Inseparable.eq
instT1Space 📖	mathematical	—	T1Space OnePoint instTopologicalSpace	—	isClosed_infty Set.image_singleton isClosed_image_coe isClosed_singleton isCompact_singleton
instTotallySeparatedSpaceOfDiscreteTopology 📖	mathematical	—	TotallySeparatedSpace OnePoint instTopologicalSpace	—	isOpen_compl_singleton instT1Space T2Space.t1Space DiscreteTopology.toT2Space isOpen_iff_of_notMem isOpen_discrete Eq.subset Set.instReflSubset Set.compl_union_self disjoint_compl_left Set.union_compl_self disjoint_compl_right
isClosed_iff_of_mem 📖	mathematical	OnePoint Set Set.instMembership infty	IsClosed instTopologicalSpace Set.preimage some	—	isOpen_compl_iff isOpen_iff_of_notMem Set.preimage_compl
isClosed_iff_of_notMem 📖	mathematical	OnePoint Set Set.instMembership infty	IsClosed instTopologicalSpace Set.preimage some IsCompact	—	isOpen_compl_iff isOpen_iff_of_mem Set.mem_compl Set.preimage_compl compl_compl
isClosed_image_coe 📖	mathematical	—	IsClosed OnePoint instTopologicalSpace Set.image some IsCompact	—	isOpen_compl_iff isOpen_compl_image_coe
isClosed_infty 📖	mathematical	—	IsClosed OnePoint instTopologicalSpace Set Set.instSingletonSet infty	—	compl_range_coe isClosed_compl_iff isOpen_range_coe
isCompl_range_coe_infty 📖	mathematical	—	IsCompl Set OnePoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instBoundedOrder Set.range some Set.instSingletonSet infty	—	Set.isCompl_range_some_none
isDenseEmbedding_coe 📖	mathematical	—	IsDenseEmbedding OnePoint instTopologicalSpace some	—	isOpenEmbedding_coe Topology.IsEmbedding.toIsInducing Topology.IsOpenEmbedding.toIsEmbedding denseRange_coe Topology.IsEmbedding.injective
isOpenEmbedding_coe 📖	mathematical	—	Topology.IsOpenEmbedding OnePoint instTopologicalSpace some	—	Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap continuous_coe coe_injective isOpenMap_coe
isOpenMap_coe 📖	mathematical	—	IsOpenMap OnePoint instTopologicalSpace some	—	isOpen_image_coe
isOpen_compl_image_coe 📖	mathematical	—	IsOpen OnePoint instTopologicalSpace Compl.compl Set Set.instCompl Set.image some IsClosed IsCompact	—	isOpen_iff_of_mem infty_notMem_image_coe Set.preimage_compl compl_compl Set.preimage_image_eq coe_injective
isOpen_def 📖	mathematical	—	IsOpen OnePoint instTopologicalSpace IsCompact Compl.compl Set Set.instCompl Set.preimage some	—	—
isOpen_iff_of_mem 📖	mathematical	OnePoint Set Set.instMembership infty	IsOpen instTopologicalSpace IsClosed Compl.compl Set.instCompl Set.preimage some IsCompact	—	isOpen_iff_of_mem'
isOpen_iff_of_mem' 📖	mathematical	OnePoint Set Set.instMembership infty	IsOpen instTopologicalSpace IsCompact Compl.compl Set.instCompl Set.preimage some	—	—
isOpen_iff_of_notMem 📖	mathematical	OnePoint Set Set.instMembership infty	IsOpen instTopologicalSpace Set.preimage some	—	instIsEmptyFalse
isOpen_image_coe 📖	mathematical	—	IsOpen OnePoint instTopologicalSpace Set.image some	—	isOpen_iff_of_notMem infty_notMem_image_coe Set.preimage_image_eq coe_injective
isOpen_range_coe 📖	mathematical	—	IsOpen OnePoint instTopologicalSpace Set.range some	—	Topology.IsOpenEmbedding.isOpen_range isOpenEmbedding_coe
le_nhds_infty 📖	mathematical	—	Filter OnePoint Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds instTopologicalSpace infty Set Filter.instMembership Set.instUnion Set.image some Compl.compl Set.instCompl Set.instSingletonSet	—	Filter.HasBasis.ge_iff hasBasis_nhds_infty
map_comp 📖	mathematical	—	map OnePoint	—	—
map_id 📖	mathematical	—	map OnePoint	—	—
map_infty 📖	mathematical	—	map infty	—	—
map_some 📖	mathematical	—	map some	—	—
ne_infty_iff_exists 📖	mathematical	—	some	—	—
nhdsNE_coe_neBot 📖	mathematical	—	Filter.NeBot OnePoint nhdsWithin instTopologicalSpace some Compl.compl Set Set.instCompl Set.instSingletonSet	—	nhdsWithin_coe Filter.NeBot.map
nhdsNE_infty_eq 📖	mathematical	—	nhdsWithin OnePoint instTopologicalSpace infty Compl.compl Set Set.instCompl Set.instSingletonSet Filter.map some Filter.coclosedCompact	—	Filter.HasBasis.ext nhdsWithin_basis_open Filter.HasBasis.map Filter.hasBasis_coclosedCompact isOpen_iff_of_mem compl_compl Set.instReflSubset Set.mem_compl infty_notMem_image_coe isOpen_compl_image_coe compl_image_coe Set.union_singleton Set.insert_diff_of_mem Set.diff_singleton_eq_self
nhdsNE_infty_neBot 📖	mathematical	—	Filter.NeBot OnePoint nhdsWithin instTopologicalSpace infty Compl.compl Set Set.instCompl Set.instSingletonSet	—	nhdsNE_infty_eq Filter.map_neBot instNeBotCoclosedCompactOfNoncompactSpace
nhdsNE_neBot 📖	mathematical	Filter.NeBot nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	OnePoint instTopologicalSpace	—	nhdsNE_infty_neBot nhdsNE_coe_neBot
nhdsWithin_coe 📖	mathematical	—	nhdsWithin OnePoint instTopologicalSpace some Filter.map Set.preimage	—	Topology.IsOpenEmbedding.map_nhdsWithin_preimage_eq isOpenEmbedding_coe
nhdsWithin_coe_image 📖	mathematical	—	nhdsWithin OnePoint instTopologicalSpace some Set.image Filter.map	—	Topology.IsEmbedding.map_nhdsWithin_eq Topology.IsOpenEmbedding.isEmbedding isOpenEmbedding_coe
nhds_coe_eq 📖	mathematical	—	nhds OnePoint instTopologicalSpace some Filter.map	—	Topology.IsOpenEmbedding.map_nhds_eq isOpenEmbedding_coe
nhds_infty_eq 📖	mathematical	—	nhds OnePoint instTopologicalSpace infty Filter Filter.instSup Filter.map some Filter.coclosedCompact Filter.instPure	—	nhdsNE_infty_eq nhdsNE_sup_pure
notMem_range_coe_iff 📖	mathematical	—	OnePoint Set Set.instMembership Set.range some infty	—	Set.mem_compl_iff compl_range_coe Set.mem_singleton_iff
not_continuous_cofiniteTopology_of_symm 📖	mathematical	—	Continuous CofiniteTopology OnePoint CofiniteTopology.instTopologicalSpace instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CofiniteTopology.of	—	Nontrivial.to_nonempty Infinite.instNontrivial CofiniteTopology.nhds_eq Equiv.symm_apply_apply nhds_coe_eq nhds_discrete Set.Finite.infinite_compl infinite Set.finite_singleton
not_inseparable_coe_infty 📖	mathematical	—	Inseparable OnePoint instTopologicalSpace some infty	—	not_specializes_infty_coe Inseparable.specializes'
not_inseparable_infty_coe 📖	mathematical	—	Inseparable OnePoint instTopologicalSpace infty some	—	not_specializes_infty_coe Inseparable.specializes
not_specializes_infty_coe 📖	mathematical	—	Specializes OnePoint instTopologicalSpace infty some	—	IsClosed.not_specializes isClosed_infty coe_ne_infty
range_coe_inter_infty 📖	mathematical	—	Set OnePoint Set.instInter Set.range some Set.instSingletonSet infty Set.instEmptyCollection	—	Set.inter_singleton_of_notMem
range_coe_union_infty 📖	mathematical	—	Set OnePoint Set.instUnion Set.range some Set.instSingletonSet infty Set.univ	—	Set.range_some_union_none
some_eq_iff 📖	mathematical	—	some	—	iff_eq_eq
specializes_coe 📖	mathematical	—	Specializes OnePoint instTopologicalSpace some	—	Topology.IsInducing.specializes_iff Topology.IsOpenEmbedding.isInducing isOpenEmbedding_coe
tendsto_coe_infty 📖	mathematical	—	Filter.Tendsto OnePoint some Filter.coclosedCompact nhds instTopologicalSpace infty	—	nhds_infty_eq Filter.Tendsto.mono_right Filter.tendsto_map le_sup_left
tendsto_nhds_infty 📖	mathematical	—	Filter.Tendsto OnePoint nhds instTopologicalSpace infty Set Set.instMembership IsClosed IsCompact Set.MapsTo some Compl.compl Set.instCompl	—	tendsto_nhds_infty' Filter.HasBasis.tendsto_left_iff Filter.hasBasis_coclosedCompact
tendsto_nhds_infty' 📖	mathematical	—	Filter.Tendsto OnePoint nhds instTopologicalSpace infty Filter Filter.instPure some Filter.coclosedCompact	—	nhds_infty_eq
ultrafilter_le_nhds_infty 📖	mathematical	—	Filter OnePoint Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Ultrafilter.toFilter nhds instTopologicalSpace infty Set Ultrafilter Ultrafilter.instMembershipSet Set.image some	—	—

(root)

Definitions

Name	Category	Theorems
OnePoint 📖	CompOp	94 math math: OnePoint.not_inseparable_infty_coe, OnePoint.isOpen_def, OnePoint.instConnectedSpaceOfPreconnectedSpaceOfNoncompactSpace, OnePoint.continuous_iff, OnePoint.nhdsWithin_coe, OnePoint.nhdsWithin_coe_image, OnePoint.isBoundedAt_iff_exists_SL2Z, OnePoint.denseRange_coe, IsCusp.smul_of_mem, OnePoint.equivOfIsEmbeddingOfRangeEq_apply_infty, OnePoint.continuousAt_infty, OnePoint.equivOfIsEmbeddingOfRangeEq_apply_coe, OnePoint.smul_infty_eq_self_iff, OnePoint.compl_infty, OnePoint.isClosed_infty, OnePoint.isZeroAt_iff_exists_SL2Z, OnePoint.infty_mem_opensOfCompl, OnePoint.isOpen_range_coe, OnePoint.notMem_range_coe_iff, OnePoint.isOpenMap_coe, OnePoint.nhdsNE_infty_neBot, OnePoint.continuous_map, OnePoint.comap_coe_nhds, OnePoint.infty_notMem_image_coe, isCusp_SL2Z_iff', OnePoint.coe_injective, OnePoint.tendsto_nhds_infty, OnePoint.smul_some_eq_ite, Rat.not_firstCountableTopology_opc, OnePoint.coe_preimage_infty, OnePoint.nhdsNE_neBot, OnePoint.compl_range_coe, OnePoint.isClosed_image_coe, OnePoint.instCompactSpace, OnePoint.map_smul, OnePoint.canLift, LightProfinite.instMetrizableSpaceOnePointNat, OnePoint.instNormalSpaceOfWeaklyLocallyCompactSpaceOfR1Space, OnePoint.nhds_coe_eq, OnePoint.IsZeroAt.smul_iff, Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff, OnePoint.map_id, Homeomorph.onePointCongr_symm_apply, isCusp_SL2Z_iff, OnePoint.map_comp, OnePoint.equivProjectivization_symm_apply_mk, OnePoint.not_specializes_infty_coe, OnePoint.isOpenEmbedding_coe, OnePoint.inseparable_coe, OnePoint.comap_coe_nhds_infty, OnePoint.smul_infty_eq_ite, OnePoint.instT0Space, OnePoint.IsBoundedAt.smul_iff, Rat.not_countably_generated_nhds_infty_opc, Rat.not_secondCountableTopology_opc, Homeomorph.onePointCongr_apply, OnePoint.compl_image_coe, OnePoint.nhdsNE_infty_eq, OnePoint.continuous_iff_from_discrete, OnePoint.hasBasis_nhds_infty, OnePoint.smul_infty_def, OnePoint.continuousAt_infty', cosetToCuspOrbit_apply_mk, OnePoint.exists_mem_SL2, OnePoint.range_coe_union_infty, OnePoint.inseparable_iff, OnePoint.not_continuous_cofiniteTopology_of_symm, OnePoint.isDenseEmbedding_coe, OnePoint.specializes_coe, OnePoint.continuous_map_iff, OnePoint.nhdsNE_coe_neBot, OnePoint.instTotallySeparatedSpaceOfDiscreteTopology, OnePoint.range_coe_inter_infty, OnePoint.continuous_coe, OnePoint.nhds_infty_eq, OnePoint.infty_notMem_range_coe, OnePoint.insert_infty_range_coe, OnePoint.ultrafilter_le_nhds_infty, OnePoint.tendsto_nhds_infty', OnePoint.tendsto_coe_infty, OnePoint.continuousAt_coe, OnePoint.equivProjectivization_apply_coe, OnePoint.not_inseparable_coe_infty, OnePoint.isOpen_compl_image_coe, OnePoint.le_nhds_infty, OnePoint.instT1Space, Matrix.GeneralLinearGroup.IsParabolic.smul_eq_self_iff, OnePoint.continuous_iff_from_nat, OnePoint.isCompl_range_coe_infty, OnePoint.infinite, LightProfinite.isClosedEmbedding_natUnionInftyEmbedding, IsCusp.smul, OnePoint.equivProjectivization_apply_infinity, OnePoint.isOpen_image_coe
instReprOnePoint 📖	CompOp	—

---

← Back to Index