Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-04 19:43 19e7b1f5

View on Github →

feat(analysis/topology): Bounded continuous functions (#464)

Estimated changes

added theorem bounded.subset
added def bounded
added theorem bounded_bUnion
added theorem bounded_ball
added theorem bounded_closed_ball
added theorem bounded_empty
added theorem bounded_of_compact
added theorem bounded_of_finite
added theorem bounded_range_iff
added theorem bounded_singleton
added theorem bounded_union
added theorem cauchy_seq_bdd
added theorem dist_triangle4
added theorem dist_triangle4_left
added theorem dist_triangle4_right
added theorem mem_of_closed'
modified theorem tendsto_at_top_metric