Documentation Verification Report

AsymptoticCone

📁 Source: Mathlib/Analysis/Normed/Affine/AsymptoticCone.lean

Statistics

Metric	Count
Definitions	0
Theorems `asymptoticNhds_le_cobounded`, `cobounded_eq_iSup_sphere_asymptoticNhds`, `asymptoticCone_subset_singleton_of_bounded`, `isBounded_iff_asymptoticCone_subset_singleton`, `not_bounded_iff_exists_ne_zero_mem_asymptoticCone`	5
Total	5

AffineSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asymptoticNhds_le_cobounded` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `asymptoticNhds` `Real` `Real.instField` `Real.linearOrder` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Bornology.cobounded` `PseudoMetricSpace.toBornology`	—	`AddTorsor.nonempty` `Filter.tendsto_id'` `Metric.tendsto_dist_right_atTop_iff` `asymptoticNhds_eq_smul_vadd` `instOrderTopologyReal` `Real.instIsStrictOrderedRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Filter.vadd_pure` `Filter.map₂_smul` `Filter.map_prod_eq_map₂` `Filter.map_map` `Filter.tendsto_map'_iff` `dist_vadd_left` `norm_smul` `NormedSpace.toNormSMulClass` `Filter.Tendsto.atTop_mul_pos` `norm_pos_iff` `Filter.Tendsto.comp` `tendsto_norm_atTop_atTop` `Filter.Tendsto.fst` `Filter.tendsto_id` `Filter.Tendsto.norm` `Filter.tendsto_snd`
`cobounded_eq_iSup_sphere_asymptoticNhds` 📖	mathematical	—	`Bornology.cobounded` `PseudoMetricSpace.toBornology` `MetricSpace.toPseudoMetricSpace` `iSup` `Filter` `Filter.instSupSet` `Set` `Set.instMembership` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne` `asymptoticNhds` `Real.instField` `Real.linearOrder` `NormedSpace.toModule` `Real.normedField` `NormedAddTorsor.toAddTorsor` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`le_antisymm` `AddTorsor.nonempty` `IsCompact.elim_nhds_subcover` `isCompact_sphere` `FiniteDimensional.proper_real` `Metric.comap_dist_left_atTop` `Filter.inter_mem` `Filter.Ioi_mem_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `Finset.iInter_mem_sets` `mem_sphere_zero_iff_norm` `norm_smul` `NormedSpace.toNormSMulClass` `norm_inv` `norm_norm` `inv_mul_cancel₀` `LT.lt.ne'` `dist_eq_norm_vsub'` `Set.mem_preimage` `Set.mem_iUnion₂` `vsub_vadd` `smul_inv_smul₀` `Set.smul_mem_smul` `Set.biInter_subset_of_mem` `Function.sometimes_spec` `Filter.vadd_pure` `asymptoticNhds_eq_smul_vadd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instOrderTopologyReal` `Real.instIsStrictOrderedRing` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `iSup₂_le` `asymptoticNhds_le_cobounded` `Metric.ne_of_mem_sphere` `one_ne_zero` `NeZero.charZero_one` `RCLike.charZero_rclike`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asymptoticCone_subset_singleton_of_bounded` 📖	mathematical	`Bornology.IsBounded` `PseudoMetricSpace.toBornology` `MetricSpace.toPseudoMetricSpace`	`Set` `Set.instHasSubset` `asymptoticCone` `Real` `Real.instField` `Real.linearOrder` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`AffineSpace.asymptoticNhds_le_cobounded`
`isBounded_iff_asymptoticCone_subset_singleton` 📖	mathematical	—	`Bornology.IsBounded` `PseudoMetricSpace.toBornology` `MetricSpace.toPseudoMetricSpace` `Set` `Set.instHasSubset` `asymptoticCone` `Real` `Real.instField` `Real.linearOrder` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`asymptoticCone_subset_singleton_of_bounded` `AffineSpace.cobounded_eq_iSup_sphere_asymptoticNhds` `Metric.ne_of_mem_sphere` `one_ne_zero` `NeZero.charZero_one` `RCLike.charZero_rclike`
`not_bounded_iff_exists_ne_zero_mem_asymptoticCone` 📖	mathematical	—	`Bornology.IsBounded` `PseudoMetricSpace.toBornology` `MetricSpace.toPseudoMetricSpace` `Set` `Set.instMembership` `asymptoticCone` `Real` `Real.instField` `Real.linearOrder` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`isBounded_iff_asymptoticCone_subset_singleton` `Set.subset_singleton_iff`

---

← Back to Index