Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-04 07:50 bd23639b

View on Github →

feat(topology/bornology): add more instances (#13621)

Estimated changes

Created src/topology/bornology/constructions.lean

added theorem bornology.cobounded_pi

added theorem bornology.cobounded_prod

added theorem bornology.forall_is_bounded_image_eval_iff

added def bornology.induced

added theorem bornology.is_bounded.fst_of_prod

added theorem bornology.is_bounded.pi

added theorem bornology.is_bounded.prod

added theorem bornology.is_bounded.snd_of_prod

added theorem bornology.is_bounded_image_fst_and_snd

added theorem bornology.is_bounded_image_subtype_coe

added theorem bornology.is_bounded_induced

added theorem bornology.is_bounded_pi

added theorem bornology.is_bounded_pi_of_nonempty

added theorem bornology.is_bounded_prod

added theorem bornology.is_bounded_prod_of_nonempty

added theorem bornology.is_bounded_prod_self

added theorem bounded_space_coe_set_iff

added theorem bounded_space_induced_iff

added theorem bounded_space_subtype_iff