Commit 2023-01-26 21:39 724a444a

View on Github →

feat: port Topology.Bornology.Constructions (#1854) porting notes:

at one point I had to explicit provide the bornology to isBounded_univ. This seems like a regression and should be investigated.

depends on: #1822

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Bornology/Constructions.lean

added theorem Bornology.IsBounded.fst_of_prod

added theorem Bornology.IsBounded.pi

added theorem Bornology.IsBounded.prod

added theorem Bornology.IsBounded.snd_of_prod

added theorem Bornology.cobounded_pi

added theorem Bornology.cobounded_prod

added theorem Bornology.forall_isBounded_image_eval_iff

added def Bornology.induced

added theorem Bornology.isBounded_image_fst_and_snd

added theorem Bornology.isBounded_image_subtype_val

added theorem Bornology.isBounded_induced

added theorem Bornology.isBounded_pi

added theorem Bornology.isBounded_pi_of_nonempty

added theorem Bornology.isBounded_prod

added theorem Bornology.isBounded_prod_of_nonempty

added theorem Bornology.isBounded_prod_self

added theorem boundedSpace_induced_iff

added theorem boundedSpace_subtype_iff

added theorem boundedSpace_val_set_iff