Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-12 08:46 36bafae8

View on Github →

feat(topology/bornology/basic): review (#13374)

add lemmas;
upgrade some implications to iffs.

Estimated changes

Modified src/topology/bornology/basic.lean

modified theorem bornology.is_bounded.subset

modified theorem bornology.is_bounded.union

modified def bornology.is_bounded

modified theorem bornology.is_bounded_Union

modified theorem bornology.is_bounded_bUnion

added theorem bornology.is_bounded_bUnion_finset

modified theorem bornology.is_bounded_sUnion

modified theorem bornology.is_bounded_singleton

added theorem bornology.is_bounded_union

added theorem bornology.is_cobounded.inter

added theorem bornology.is_cobounded.superset

added theorem bornology.is_cobounded_Inter

added theorem bornology.is_cobounded_bInter

added theorem bornology.is_cobounded_bInter_finset

added theorem bornology.is_cobounded_inter

added theorem bornology.is_cobounded_sInter

added theorem bornology.is_cobounded_univ

modified theorem bornology.sUnion_bounded_univ