Instances

Statistics

Metric	Count
Definitions	0
Theorems `instCompletableTopField`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompletableTopField` 📖	mathematical	—	`CompletableTopField` `toField` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `toNormedCommRing`	—	`T3Space.toT0Space` `T4Space.t3Space` `instT4SpaceOfT1SpaceOfNormalSpace` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `CompletelyNormalSpace.toNormalSpace` `UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity` `EMetric.instIsCountablyGeneratedUniformity` `SeminormedAddGroup.disjoint_nhds_zero` `disjoint_iff` `Filter.Eventually.mono` `le_inv_of_le_inv₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `norm_inv` `inv_inv` `LT.lt.trans_le` `mul_sub` `inv_mul_cancel₀` `sub_mul` `mul_inv_cancel_right₀` `one_mul` `IsUniformAddGroup.cauchy_map_iff_tendsto` `SeminormedAddCommGroup.to_isUniformAddGroup` `Filter.tendsto_congr'` `IsUniformAddGroup.cauchy_iff_tendsto_swapped` `Filter.Tendsto.zero_mul_isBoundedUnder_le` `Filter.isBoundedUnder_le_mul_tendsto_zero` `Filter.Tendsto.isBoundedUnder_comp` `Filter.tendsto_fst` `Filter.tendsto_snd`

---