Completion

📁 Source: Mathlib/Analysis/Asymptotics/Completion.lean

Statistics

Metric	Count
Definitions	0
Theorems isBigO_completion_left, isBigO_completion_right, isLittleO_completion_left, isLittleO_completion_right, isTheta_completion_left, isTheta_completion_right	6
Total	6

Asymptotics

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBigO_completion_left 📖	mathematical	—	IsBigO UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace UniformSpace.Completion.instNorm SeminormedAddCommGroup.toNorm UniformSpace.Completion.coe'	—	UniformSpace.Completion.norm_coe
isBigO_completion_right 📖	mathematical	—	IsBigO UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace UniformSpace.Completion.instNorm SeminormedAddCommGroup.toNorm UniformSpace.Completion.coe'	—	UniformSpace.Completion.norm_coe
isLittleO_completion_left 📖	mathematical	—	IsLittleO UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace UniformSpace.Completion.instNorm SeminormedAddCommGroup.toNorm UniformSpace.Completion.coe'	—	UniformSpace.Completion.norm_coe
isLittleO_completion_right 📖	mathematical	—	IsLittleO UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace UniformSpace.Completion.instNorm SeminormedAddCommGroup.toNorm UniformSpace.Completion.coe'	—	UniformSpace.Completion.norm_coe
isTheta_completion_left 📖	mathematical	—	IsTheta UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace UniformSpace.Completion.instNorm SeminormedAddCommGroup.toNorm UniformSpace.Completion.coe'	—	isBigO_completion_left isBigO_completion_right
isTheta_completion_right 📖	mathematical	—	IsTheta UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace UniformSpace.Completion.instNorm SeminormedAddCommGroup.toNorm UniformSpace.Completion.coe'	—	isBigO_completion_right isBigO_completion_left

---

← Back to Index