Mathlib Changelog
v3
Changelog
About
Github
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
iff
s.
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