Lemmas

Statistics

Metric	Count
Definitions	0
Theorems `eventually_nnnorm_sub_lt`, `eventually_norm_sub_lt`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_nnnorm_sub_lt` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`Filter.Eventually` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`ContinuousAt.nnnorm` `ContinuousAt.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuousAt_id` `continuousAt_const` `gt_mem_nhds` `NNReal.instOrderTopology` `sub_self` `nnnorm_zero`
`eventually_norm_sub_lt` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Filter.Eventually` `Norm.norm` `SeminormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`ContinuousAt.norm` `ContinuousAt.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuousAt_id` `continuousAt_const` `gt_mem_nhds` `instOrderTopologyReal` `sub_self` `norm_zero`

---