Mathlib Changelog
Changelog
About
Github
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