Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-20 20:14 656f7494

View on Github →

feat(analysis/locally_convex): define von Neumann boundedness (#12449) Define the von Neumann boundedness and show elementary properties, including that it defines a bornology.

Estimated changes

Created src/analysis/locally_convex/bounded.lean

added theorem bornology.is_bounded_iff_is_vonN_bounded

added theorem bornology.is_vonN_bounded.of_topological_space_le

added theorem bornology.is_vonN_bounded.subset

added theorem bornology.is_vonN_bounded.union

added def bornology.is_vonN_bounded

added theorem bornology.is_vonN_bounded_covers

added theorem bornology.is_vonN_bounded_empty

added theorem bornology.is_vonN_bounded_iff

added theorem bornology.is_vonN_bounded_singleton

added def bornology.vonN_bornology

Modified src/topology/bornology/basic.lean

added theorem bornology.is_bounded_of_bounded_iff

added theorem bornology.is_cobounded_of_bounded_iff