Commit 2023-04-26 23:45 850e6705

View on Github →

feat: port Analysis.LocallyConvex.Bounded (#3656)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/LocallyConvex/Bounded.lean

added theorem Bornology.IsVonNBounded.image

added theorem Bornology.IsVonNBounded.of_topologicalSpace_le

added theorem Bornology.IsVonNBounded.smul_tendsto_zero

added theorem Bornology.IsVonNBounded.subset

added theorem Bornology.IsVonNBounded.union

added def Bornology.IsVonNBounded

added theorem Bornology.isBounded_iff_isVonNBounded

added theorem Bornology.isVonNBounded_covers

added theorem Bornology.isVonNBounded_empty

added theorem Bornology.isVonNBounded_iff

added theorem Bornology.isVonNBounded_iff_smul_tendsto_zero

added theorem Bornology.isVonNBounded_of_smul_tendsto_zero

added theorem Bornology.isVonNBounded_singleton

added def Bornology.vonNBornology

added theorem Filter.HasBasis.isVonNBounded_basis_iff

added theorem NormedSpace.image_isVonNBounded_iff

added theorem NormedSpace.isBounded_iff_subset_smul_ball

added theorem NormedSpace.isBounded_iff_subset_smul_closedBall

added theorem NormedSpace.isVonNBounded_ball

added theorem NormedSpace.isVonNBounded_closedBall

added theorem NormedSpace.isVonNBounded_iff'

added theorem NormedSpace.isVonNBounded_iff

added theorem NormedSpace.vonNBornology_eq

added theorem TotallyBounded.isVonNBounded