Pi

📁 Source: Mathlib/Topology/UniformSpace/Pi.lean

Statistics

Metric	Count
Definitions Pi, Pi, uniformSpace	3
Theorems pi, iInf, complete, uniformContinuous_postcomp, uniformContinuous_postcomp', uniformContinuous_precomp, uniformContinuous_precomp', uniformContinuous_proj, uniformContinuous_restrict, uniformSpace_comap_precomp, uniformSpace_comap_precomp', uniformSpace_comap_restrict, uniformSpace_comap_restrict_sUnion, uniformSpace_eq, uniformity, cauchy_pi_iff, cauchy_pi_iff', instIsCountablyGeneratedProdForallUniformityOfCountable, uniformContinuous_pi	19
Total	22

Cauchy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pi 📖	mathematical	Cauchy	Pi.uniformSpace Filter.pi	—	Filter.map_eval_pi

CompleteSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iInf 📖	mathematical	CompleteSpace T2Space TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder UniformSpace.toTopologicalSpace	iInf UniformSpace instInfSetUniformSpace	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim complete_of_compact Finite.compactSpace Finite.of_subsingleton iInf_uniformity Pi.uniformity Filter.comap_iInf Filter.comap_comap Filter.comap_id' completeSpace_iff_isComplete_range Set.range_const_eq_diagonal Nontrivial.to_nonempty Set.setOf_forall iInf_mono induced_mono IsClosed.isComplete Pi.complete IsClosed.mono isClosed_iInter isClosed_eq continuous_apply

HomotopyGroup

Definitions

Name	Category	Theorems
Pi 📖	CompOp	—

MvQPF

Definitions

Name	Category	Theorems
Pi 📖	CompOp	—

Pi

Definitions

Name	Category	Theorems
uniformSpace 📖	CompOp	71 math math: uniformSpace_eq, uniformContinuous_postcomp', UniformEquiv.funUnique_apply, cauchy_pi_iff', IsUltraUniformity.pi, PiLp.toEquiv_uniformEquiv, UniformEquiv.piCongrLeft_refl, CStarMatrix.toCLM_injective, uniformSpace_comap_precomp, CStarMatrix.norm_def', CStarMatrix.inner_toCLM_conjTranspose_left, uniformContinuous_precomp', CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM, uniformSpace_comap_restrict, uniformContinuous_proj, uniformSpace_comap_precomp', uniformContinuous_postcomp, UniformEquiv.piCongrLeft_symm_apply, BoundedContinuousFunction.uniformContinuous_coe, UniformEquiv.finTwoArrow_apply, CStarMatrix.toCLM_apply_single, CStarMatrix.toCLM_apply_eq_sum, Equicontinuous.comap_uniformFun_eq, UniformEquiv.finTwoArrow_symm_apply, CStarMatrix.toCLM_apply, UniformOnFun.uniformContinuous_toFun, ContinuousAlternatingMap.uniformContinuous_coe_fun, CStarMatrix.mul_entry_mul_eq_inner_toCLM, ContDiffMapSupportedIn.isUniformEmbedding_pi_structureMapCLM, EquicontinuousOn.comap_uniformOnFun_eq, Equicontinuous.isUniformInducing_uniformFun_iff_pi, UniformEquiv.piCongrLeft_toEquiv, UniformEquiv.funUnique_symm_apply, PiLp.toHomeomorph_uniformEquiv, EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi, instIsCountablyGeneratedProdForallUniformityOfCountable, instIsUniformGroup, ContinuousMultilinearMap.uniformContinuous_coe_fun, PiLp.isUniformInducing_toLp, UniformEquiv.piCongr_toEquiv, Cauchy.pi, UniformOnFun.uniformContinuous_restrict_toFun, uniformContinuous_pi, UniformEquiv.piCongrRight_refl, complete, PiLp.uniformContinuous_ofLp, cauchy_pi_iff, uniformSpace_comap_restrict_sUnion, PiLp.uniformContinuous_toLp, UniformFun.uniformContinuous_toFun, UniformOnFun.isUniformEmbedding_toFun_finite, UniformEquiv.piCongr_apply, UniformOnFun.isUniformInducing_pi_restrict, lp.uniformContinuous_coe, UniformEquiv.piCongrLeft_apply_apply, uniformContinuous_restrict, Metric.PiNatEmbed.isUniformEmbedding_embed, UniformEquiv.piCongrRight_symm, instIsUniformAddGroup, PointwiseConvergenceCLM.isUniformEmbedding_coeFn, UniformEquiv.piFinTwo_symm_apply, UniformEquiv.piCongrLeft_apply, UniformEquiv.piFinTwo_apply, EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi', UniformEquiv.piCongrRight_toEquiv, CStarMatrix.norm_def, uniformContinuous_precomp, CStarMatrix.inner_toCLM_conjTranspose_right, CStarMatrix.toCLM_apply_single_apply, uniformity, UniformEquiv.piCongrRight_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
complete 📖	mathematical	CompleteSpace	uniformSpace	—	nhds_pi Filter.le_pi Filter.map_neBot
uniformContinuous_postcomp 📖	mathematical	UniformContinuous	uniformSpace	—	uniformContinuous_postcomp'
uniformContinuous_postcomp' 📖	mathematical	UniformContinuous	uniformSpace	—	uniformContinuous_pi UniformContinuous.comp uniformContinuous_proj
uniformContinuous_precomp 📖	mathematical	—	UniformContinuous uniformSpace	—	uniformContinuous_precomp'
uniformContinuous_precomp' 📖	mathematical	—	UniformContinuous uniformSpace	—	uniformContinuous_pi uniformContinuous_proj
uniformContinuous_proj 📖	mathematical	—	UniformContinuous uniformSpace	—	uniformContinuous_pi uniformContinuous_id
uniformContinuous_restrict 📖	mathematical	—	UniformContinuous uniformSpace Set.Elem Set Set.instMembership Set.restrict	—	uniformContinuous_precomp'
uniformSpace_comap_precomp 📖	mathematical	—	UniformSpace.comap uniformSpace iInf UniformSpace instInfSetUniformSpace Function.eval	—	uniformSpace_comap_precomp'
uniformSpace_comap_precomp' 📖	mathematical	—	UniformSpace.comap uniformSpace iInf UniformSpace instInfSetUniformSpace Function.eval	—	uniformSpace_eq UniformSpace.comap_iInf
uniformSpace_comap_restrict 📖	mathematical	—	UniformSpace.comap Set.restrict uniformSpace Set.Elem Set Set.instMembership iInf UniformSpace instInfSetUniformSpace Function.eval	—	iInf_congr_Prop uniformSpace_comap_precomp'
uniformSpace_comap_restrict_sUnion 📖	mathematical	—	UniformSpace.comap Set.restrict Set.sUnion uniformSpace Set.Elem Set Set.instMembership iInf UniformSpace instInfSetUniformSpace	—	uniformSpace_comap_restrict iInf_congr_Prop iInf_sUnion
uniformSpace_eq 📖	mathematical	—	uniformSpace iInf UniformSpace instInfSetUniformSpace UniformSpace.comap Function.eval	—	UniformSpace.ext
uniformity 📖	mathematical	—	uniformity uniformSpace iInf Filter Filter.instInfSet Filter.comap	—	iInf_uniformity

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchy_pi_iff 📖	mathematical	—	Cauchy Pi.uniformSpace Filter.map Function.eval	—	Pi.uniformSpace_eq
cauchy_pi_iff' 📖	mathematical	—	Cauchy Pi.uniformSpace Filter.map Function.eval	—	Pi.uniformSpace_eq
instIsCountablyGeneratedProdForallUniformityOfCountable 📖	mathematical	Filter.IsCountablyGenerated uniformity	Pi.uniformSpace	—	Pi.uniformity Filter.iInf.isCountablyGenerated Filter.comap.isCountablyGenerated
uniformContinuous_pi 📖	mathematical	—	UniformContinuous Pi.uniformSpace	—	Pi.uniformity

---

← Back to Index