Bounded

📁 Source: Mathlib/Analysis/LocallyConvex/Bounded.lean

Statistics

Metric	Count
Definitions `IsVonNBounded`, `vonNBornology`, `QuasiCompleteSpace`	3
Theorems `add`, `closure`, `extend_scalars`, `image`, `insert`, `neg`, `of_add_left`, `of_add_right`, `of_boundedSpace`, `of_neg`, `of_sub_left`, `of_sub_right`, `of_subsingleton`, `of_topologicalSpace_le`, `restrict_scalars`, `restrict_scalars_of_nontrivial`, `smul_tendsto_zero`, `sub`, `subset`, `tendsto_smallSets_nhds`, `union`, `vadd`, `isBounded_iff_isVonNBounded`, `isVonNBounded_add`, `isVonNBounded_add_of_nonempty`, `isVonNBounded_add_self`, `isVonNBounded_biUnion`, `isVonNBounded_covers`, `isVonNBounded_empty`, `isVonNBounded_iUnion`, `isVonNBounded_iff`, `isVonNBounded_iff_absorbing_le`, `isVonNBounded_iff_smul_tendsto_zero`, `isVonNBounded_iff_tendsto_smallSets_nhds`, `isVonNBounded_insert`, `isVonNBounded_neg`, `isVonNBounded_of_smul_tendsto_zero`, `isVonNBounded_pi_iff`, `isVonNBounded_sUnion`, `isVonNBounded_singleton`, `isVonNBounded_sub`, `isVonNBounded_sub_of_nonempty`, `isVonNBounded_union`, `isVonNBounded_vadd`, `sUnion_isVonNBounded_eq_univ`, `isVonNBounded_iff`, `isVonNBounded_range`, `image_isVonNBounded_iff`, `isBounded_iff_subset_smul_ball`, `isBounded_iff_subset_smul_closedBall`, `isVonNBounded_ball`, `isVonNBounded_closedBall`, `isVonNBounded_iff`, `isVonNBounded_iff'`, `isVonNBounded_of_isBounded`, `vonNBornology_eq`, `quasiComplete`, `isVonNBounded`, `isVonNBounded`, `instQuasiCompleteSpaceOfCompleteSpace`, `isCompact_closure_of_totallyBounded_quasiComplete`	61
Total	64

Bornology

Definitions

Name	Category	Theorems
`IsVonNBounded` 📖	MathDef	60 math math: `withSeminorms_iff_mem_nhds_isVonNBounded`, `Bundle.ContMDiffRiemannianMetric.isVonNBounded`, `isVonNBounded_iff_tendsto_smallSets_nhds`, `WithSeminorms.image_isVonNBounded_iff_seminorm_bounded`, `isVonNBounded_add_of_nonempty`, `isVonNBounded_empty`, `isVonNBounded_add_self`, `NormedSpace.isVonNBounded_iff`, `NormedSpace.image_isVonNBounded_iff`, `isVonNBounded_pi_iff`, `ContinuousLinearMap.nhds_zero_eq_of_basis`, `Bundle.RiemannianMetric.isVonNBounded`, `isVonNBounded_neg`, `ContinuousLinearMap.hasBasis_nhds_zero`, `NormedSpace.isVonNBounded_ball`, `isVonNBounded_iff_absorbing_le`, `isVonNBounded_covers`, `isVonNBounded_iUnion`, `NormedSpace.isVonNBounded_closedBall`, `ContinuousMultilinearMap.range_toUniformOnFun`, `isVonNBounded_sub_of_nonempty`, `WithSeminorms.isVonNBounded_iff_seminorm_bddAbove`, `isVonNBounded_iff`, `TotallyBounded.isVonNBounded`, `ContinuousMultilinearMap.hasBasis_nhds_zero`, `isVonNBounded_union`, `NormedSpace.isVonNBounded_iff'`, `isVonNBounded_iff_smul_tendsto_zero`, `ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun`, `NormedSpace.isVonNBounded_of_isBounded`, `WithSeminorms.isVonNBounded_iff_finset_seminorm_bounded`, `ContinuousAlternatingMap.hasBasis_nhds_zero`, `isBounded_iff_isVonNBounded`, `ContinuousLinearMap.isVonNBounded_iff`, `ContinuousMultilinearMap.isEmbedding_toUniformOnFun`, `isVonNBounded_sUnion`, `ContinuousLinearMap.hasBasis_nhds_zero_of_basis`, `IsVonNBounded.of_subsingleton`, `isVonNBounded_sub`, `Filter.Tendsto.isVonNBounded_range`, `ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis`, `ContinuousAlternatingMap.hasBasis_nhds_zero_of_basis`, `isVonNBounded_add`, `ContinuousLinearMap.nhds_zero_eq`, `WithSeminorms.image_isVonNBounded_iff_finset_seminorm_bounded`, `Filter.HasBasis.isVonNBounded_iff`, `isVonNBounded_vadd`, `ContinuousMultilinearMap.toUniformOnFun_toFun`, `isVonNBounded_insert`, `isVonNBounded_biUnion`, `IsVonNBounded.of_boundedSpace`, `ContinuousLinearMap.isUniformEmbedding_toUniformOnFun`, `WithSeminorms.isVonNBounded_iff_seminorm_bounded`, `isVonNBounded_singleton`, `isVonNBounded_of_smul_tendsto_zero`, `sUnion_isVonNBounded_eq_univ`, `UniformConvergenceCLM.isVonNBounded_iff`, `ContinuousMultilinearMap.isUniformInducing_toUniformOnFun`, `Set.Finite.isVonNBounded`, `Bundle.ContinuousRiemannianMetric.isVonNBounded`
`vonNBornology` 📖	CompOp	2 math math: `isBounded_iff_isVonNBounded`, `NormedSpace.vonNBornology_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBounded_iff_isVonNBounded` 📖	mathematical	—	`IsBounded` `vonNBornology` `IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`isBounded_ofBounded_iff` `isVonNBounded_singleton`
`isVonNBounded_add` 📖	mathematical	—	`IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Set.instEmptyCollection`	—	`Set.eq_empty_or_nonempty` `Set.empty_add` `Set.add_empty` `isVonNBounded_add_of_nonempty` `Set.Nonempty.ne_empty`
`isVonNBounded_add_of_nonempty` 📖	mathematical	`Set.Nonempty`	`IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`IsVonNBounded.of_add_left` `IsVonNBounded.of_add_right` `IsVonNBounded.add`
`isVonNBounded_add_self` 📖	mathematical	—	`IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`Set.eq_empty_or_nonempty` `Set.add_empty`
`isVonNBounded_biUnion` 📖	mathematical	—	`IsVonNBounded` `Set.iUnion` `Set` `Set.instMembership`	—	`Set.Finite.to_subtype` `Set.biUnion_eq_iUnion` `isVonNBounded_iUnion`
`isVonNBounded_covers` 📖	mathematical	—	`Set.sUnion` `setOf` `Set` `IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set.univ`	—	`sUnion_isVonNBounded_eq_univ`
`isVonNBounded_empty` 📖	mathematical	—	`IsVonNBounded` `Set` `Set.instEmptyCollection`	—	`Absorbs.empty`
`isVonNBounded_iUnion` 📖	mathematical	—	`IsVonNBounded` `Set.iUnion`	—	`forall_swap`
`isVonNBounded_iff` 📖	mathematical	—	`IsVonNBounded` `Absorbs` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace`	—	—
`isVonNBounded_iff_absorbing_le` 📖	mathematical	—	`IsVonNBounded` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.absorbing` `DivisionSemiring.toGroupWithZero` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `DistribMulAction.toMulAction` `GroupWithZero.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `nhds`	—	—
`isVonNBounded_iff_smul_tendsto_zero` 📖	mathematical	`Filter.Tendsto` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	`IsVonNBounded` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Pi.smul'` `nhds`	—	`IsVonNBounded.smul_tendsto_zero` `Filter.Eventually.of_forall` `le_trans` `nhdsWithin_le_nhds` `isVonNBounded_of_smul_tendsto_zero` `self_mem_nhdsWithin`
`isVonNBounded_iff_tendsto_smallSets_nhds` 📖	mathematical	—	`IsVonNBounded` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Filter.Tendsto` `Set` `Set.smulSet` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Filter.smallSets`	—	`Filter.tendsto_smallSets_iff` `absorbs_iff_eventually_nhds_zero` `mem_of_mem_nhds`
`isVonNBounded_insert` 📖	mathematical	—	`IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Set.instInsert`	—	—
`isVonNBounded_neg` 📖	mathematical	—	`IsVonNBounded` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Set` `Set.neg` `NegZeroClass.toNeg`	—	`IsVonNBounded.neg` `neg_neg`
`isVonNBounded_of_smul_tendsto_zero` 📖	mathematical	`Filter.Eventually` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Filter.Tendsto` `Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	—	`Filter.HasBasis.isVonNBounded_iff` `nhds_basis_balanced` `NormedField.nhdsNE_neBot` `Mathlib.Tactic.Push.not_forall_eq` `Filter.mp_mem` `Filter.univ_mem'` `absorbs_iff_norm` `Set.not_subset` `Balanced.smul_mono` `NormedSpace.toNormSMulClass` `IsScalarTower.left` `Set.mem_inv_smul_set_iff₀` `Filter.Eventually.choice` `Filter.frequently_false` `Filter.Eventually.frequently` `Filter.Tendsto.eventually` `Filter.eventually_mem_set`
`isVonNBounded_pi_iff` 📖	mathematical	—	`IsVonNBounded` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `Pi.instSMul` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Pi.instZero` `Pi.topologicalSpace` `AddZero.toZero` `AddZeroClass.toAddZero` `Set.image` `Function.eval`	—	`nhds_pi` `Filter.smallSets_iInf` `Filter.smallSets_comap_eq_comap_image` `Set.image_image` `Set.image_congr`
`isVonNBounded_sUnion` 📖	mathematical	—	`IsVonNBounded` `Set.sUnion`	—	`Set.sUnion_eq_biUnion` `isVonNBounded_biUnion`
`isVonNBounded_singleton` 📖	mathematical	—	`IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Set.instSingletonSet`	—	`Absorbent.absorbs` `absorbent_nhds_zero`
`isVonNBounded_sub` 📖	mathematical	—	`IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Set.sub` `SubNegMonoid.toSub` `Set.instEmptyCollection`	—	`sub_eq_add_neg` `IsTopologicalAddGroup.toContinuousAdd`
`isVonNBounded_sub_of_nonempty` 📖	mathematical	`Set.Nonempty`	`IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Set.sub` `SubNegMonoid.toSub`	—	`sub_eq_add_neg` `IsTopologicalAddGroup.toContinuousAdd`
`isVonNBounded_union` 📖	mathematical	—	`IsVonNBounded` `Set` `Set.instUnion`	—	—
`isVonNBounded_vadd` 📖	mathematical	—	`IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `addGroupIsAddTorsor`	—	`neg_vadd_vadd` `IsVonNBounded.vadd`
`sUnion_isVonNBounded_eq_univ` 📖	mathematical	—	`Set.sUnion` `setOf` `Set` `IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set.univ`	—	`Set.eq_univ_iff_forall` `Set.mem_sUnion` `isVonNBounded_singleton` `Set.mem_singleton`

Bornology.IsVonNBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Bornology.IsVonNBounded` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `DistribSMul.toSMulZeroClass`	`Set` `Set.add` `AddZero.toAdd`	—	`exists_open_nhds_zero_add_subset` `Absorbs.mono_left` `Absorbs.add` `IsOpen.mem_nhds`
`closure` 📖	mathematical	`Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`closure`	—	`exists_mem_nhds_isClosed_subset` `Filter.mp_mem` `Filter.univ_mem'` `Mathlib.Tactic.GCongr.rel_imp_rel` `Set.instIsTransSubset` `closure_mono` `subset_refl` `Set.instReflSubset` `closure_smul₀` `Set.smul_set_mono` `closure_subset_iff_isClosed`
`extend_scalars` 📖	—	`Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—	`Filter.exists_seq_tendsto` `TopologicalSpace.isCountablyGenerated_nhdsWithin` `FirstCountableTopology.nhds_generated_countable` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `NormedField.nhdsNE_neBot` `Bornology.isVonNBounded_of_smul_tendsto_zero` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `Field.isDomain` `GroupWithZero.toNoZeroSMulDivisors` `IsDomain.toIsCancelMulZero` `NeZero.one` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `smul_tendsto_zero` `Filter.Eventually.of_forall` `smul_one_smul`
`image` 📖	mathematical	`Bornology.IsVonNBounded` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Set.image` `DFunLike.coe` `ContinuousLinearMap` `ContinuousLinearMap.funLike`	—	`Topology.IsEmbedding.map_nhds_eq` `Isometry.isEmbedding` `RingHom.isometry` `Function.Surjective.range_eq` `RingHom.surjective` `nhdsWithin_univ` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Continuous.tendsto'` `ContinuousLinearMap.continuous` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `image_smul_setₛₗ` `SemilinearMapClass.toMulActionSemiHomClass` `Filter.Tendsto.comp` `Filter.Tendsto.image_smallSets`
`insert` 📖	mathematical	`Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Set` `Set.instInsert`	—	`Bornology.isVonNBounded_insert`
`neg` 📖	mathematical	`Bornology.IsVonNBounded` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`Set` `Set.neg` `NegZeroClass.toNeg`	—	`neg_neg` `Absorbs.neg_neg` `neg_mem_nhds_zero`
`of_add_left` 📖	—	`Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Set.Nonempty`	—	—	`of_add_right` `add_comm`
`of_add_right` 📖	—	`Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Set.Nonempty`	—	—	`Bornology.isVonNBounded_vadd` `subset` `Set.image_subset_image2_right`
`of_boundedSpace` 📖	mathematical	—	`Bornology.IsVonNBounded`	—	`Absorbs.of_boundedSpace`
`of_neg` 📖	—	`Bornology.IsVonNBounded` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Set` `Set.neg` `NegZeroClass.toNeg`	—	—	`Bornology.isVonNBounded_neg`
`of_sub_left` 📖	—	`Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Set.sub` `SubNegMonoid.toSub` `Set.Nonempty`	—	—	`of_add_left` `sub_eq_add_neg` `Set.Nonempty.neg`
`of_sub_right` 📖	—	`Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Set.sub` `SubNegMonoid.toSub` `Set.Nonempty`	—	—	`of_neg` `of_add_right` `IsTopologicalAddGroup.toContinuousAdd` `sub_eq_add_neg`
`of_subsingleton` 📖	mathematical	—	`Bornology.IsVonNBounded`	—	`Filter.Eventually.of_forall` `Set.subset_univ` `Subsingleton.eq_univ_of_nonempty` `Set.Nonempty.image` `Filter.nonempty_of_mem` `nhds_neBot`
`of_topologicalSpace_le` 📖	—	`TopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder` `Bornology.IsVonNBounded` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—	`le_iff_nhds`
`restrict_scalars` 📖	mathematical	`Bornology.IsVonNBounded` `NormedRing.toSeminormedRing` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `MulActionWithZero.toSMulWithZero`	`SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	—	`subsingleton_or_nontrivial` `MulActionWithZero.subsingleton` `of_subsingleton` `restrict_scalars_of_nontrivial`
`restrict_scalars_of_nontrivial` 📖	mathematical	`Bornology.IsVonNBounded` `NormedRing.toSeminormedRing` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `MulAction.toSemigroupAction`	`SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	—	`Absorbs.restrict_scalars` `AntilipschitzWith.tendsto_cobounded` `AntilipschitzWith.of_le_mul_nndist` `nndist_eq_nnnorm` `sub_smul` `nnnorm_smul` `NormedSpace.toNormSMulClass` `div_eq_inv_mul` `mul_div_cancel_right₀` `GroupWithZero.toMulDivCancelClass` `nnnorm_ne_zero_iff` `one_ne_zero` `NeZero.one` `le_refl`
`smul_tendsto_zero` 📖	mathematical	`Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Filter.Eventually` `Set` `Set.instMembership` `Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing`	`Pi.smul'`	—	`Filter.Tendsto.of_smallSets` `Filter.Tendsto.comp` `tendsto_smallSets_nhds` `Filter.Eventually.mono` `Set.smul_mem_smul_set`
`sub` 📖	mathematical	`Bornology.IsVonNBounded` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`Set` `Set.sub` `SubNegMonoid.toSub`	—	`sub_eq_add_neg` `add` `IsTopologicalAddGroup.toContinuousAdd` `neg`
`subset` 📖	—	`Set` `Set.instHasSubset` `Bornology.IsVonNBounded`	—	—	`Absorbs.mono_right`
`tendsto_smallSets_nhds` 📖	mathematical	`Bornology.IsVonNBounded` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Filter.Tendsto` `Set` `Set.smulSet` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Filter.smallSets`	—	`Bornology.isVonNBounded_iff_tendsto_smallSets_nhds`
`union` 📖	mathematical	`Bornology.IsVonNBounded`	`Set` `Set.instUnion`	—	`Bornology.isVonNBounded_union`
`vadd` 📖	mathematical	`Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `addGroupIsAddTorsor`	—	`Set.singleton_vadd` `add` `Bornology.isVonNBounded_singleton`

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isVonNBounded_iff` 📖	mathematical	`Filter.HasBasis` `nhds`	`Bornology.IsVonNBounded` `Absorbs` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace`	—	`mem_of_mem` `mem_iff` `Absorbs.mono_left`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isVonNBounded_range` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds`	`Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set.range`	—	`TotallyBounded.isVonNBounded` `isUniformAddGroup_of_addCommGroup` `CauchySeq.totallyBounded_range` `cauchySeq`

NormedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_isVonNBounded_iff` 📖	mathematical	—	`Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set.image` `Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	—
`isBounded_iff_subset_smul_ball` 📖	mathematical	—	`Bornology.IsBounded` `PseudoMetricSpace.toBornology` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instHasSubset` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `Metric.ball` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Real` `Real.instOne`	—	`isVonNBounded_iff` `Absorbs.exists_pos` `Metric.ball_mem_nhds` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `NormedField.exists_lt_norm` `LT.lt.le` `Bornology.IsVonNBounded.subset` `Bornology.IsVonNBounded.image` `RingHomSurjective.ids` `RingHomIsometric.ids` `isVonNBounded_ball` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `toIsBoundedSMul`
`isBounded_iff_subset_smul_closedBall` 📖	mathematical	—	`Bornology.IsBounded` `PseudoMetricSpace.toBornology` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instHasSubset` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `Metric.closedBall` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Real` `Real.instOne`	—	`isBounded_iff_subset_smul_ball` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.smul_set_mono` `Metric.ball_subset_closedBall` `isVonNBounded_iff` `Bornology.IsVonNBounded.subset` `Bornology.IsVonNBounded.image` `RingHomSurjective.ids` `RingHomIsometric.ids` `isVonNBounded_closedBall` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `toIsBoundedSMul`
`isVonNBounded_ball` 📖	mathematical	—	`Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.ball`	—	`isVonNBounded_of_isBounded` `Metric.isBounded_ball`
`isVonNBounded_closedBall` 📖	mathematical	—	`Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Metric.closedBall`	—	`isVonNBounded_of_isBounded` `Metric.isBounded_closedBall`
`isVonNBounded_iff` 📖	mathematical	—	`Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Bornology.IsBounded` `PseudoMetricSpace.toBornology`	—	`Absorbs.exists_pos` `Metric.ball_mem_nhds` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `NormedField.exists_lt_norm` `Bornology.IsBounded.subset` `Metric.isBounded_ball` `ball_normSeminorm` `Seminorm.smul_ball_zero` `norm_pos_iff` `LT.lt.trans` `LT.lt.le` `isVonNBounded_of_isBounded`
`isVonNBounded_iff'` 📖	mathematical	—	`Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	`isVonNBounded_iff` `isBounded_iff_forall_norm_le`
`isVonNBounded_of_isBounded` 📖	mathematical	`Bornology.IsBounded` `PseudoMetricSpace.toBornology` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`Bornology.IsBounded.subset_ball` `Filter.HasBasis.isVonNBounded_iff` `Metric.nhds_basis_ball` `ball_normSeminorm` `Absorbs.mono_right` `Seminorm.ball_zero_absorbs_ball_zero`
`vonNBornology_eq` 📖	mathematical	—	`Bornology.vonNBornology` `NontriviallyNormedField.toNormedField` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsBoundedSMul.continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `toIsBoundedSMul` `PseudoMetricSpace.toBornology`	—	`IsBoundedSMul.continuousSMul` `toIsBoundedSMul` `Bornology.ext_iff_isBounded` `Bornology.isBounded_iff_isVonNBounded` `isVonNBounded_iff`

QuasiCompleteSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quasiComplete` 📖	mathematical	`Bornology.IsVonNBounded` `UniformSpace.toTopologicalSpace`	`IsComplete`	—	—

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isVonNBounded` 📖	mathematical	—	`Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Absorbent.absorbs_finite` `absorbent_nhds_zero`

TotallyBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isVonNBounded` 📖	mathematical	`TotallyBounded`	`Bornology.IsVonNBounded` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `UniformSpace.toTopologicalSpace`	—	`Continuous.tendsto'` `continuous_add` `IsTopologicalAddGroup.toContinuousAdd` `IsUniformAddGroup.to_topologicalAddGroup` `zero_add` `Filter.HasBasis.prod` `nhds_basis_balanced` `NormedField.nhdsNE_neBot` `Filter.Tendsto.basis_left` `totallyBounded_iff_subset_finite_iUnion_nhds_zero` `Absorbs.mono_right` `Set.Finite.absorbs_biUnion` `Set.add_subset_iff` `Set.mk_mem_prod` `Absorbs.mono_left` `Absorbent.vadd_absorbs` `absorbent_nhds_zero` `Balanced.absorbs_self` `Bornology.IsVonNBounded.of_boundedSpace` `Metric.isBounded_iff` `dist_eq_norm`

(root)

Definitions

Name	Category	Theorems
`QuasiCompleteSpace` 📖	CompData	1 math math: `instQuasiCompleteSpaceOfCompleteSpace`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instQuasiCompleteSpaceOfCompleteSpace` 📖	mathematical	—	`QuasiCompleteSpace`	—	`IsClosed.isComplete`
`isCompact_closure_of_totallyBounded_quasiComplete` 📖	mathematical	`TotallyBounded`	`IsCompact` `UniformSpace.toTopologicalSpace` `closure`	—	`TotallyBounded.isCompact_of_isComplete` `TotallyBounded.closure` `QuasiCompleteSpace.quasiComplete` `TotallyBounded.isVonNBounded` `isClosed_closure`

---

← Back to Index