Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-15 15:45 aa35f363

View on Github →

feat(analysis/hofer): Hofer's lemma (#3064) Adds Hofer's lemma about complete metric spaces, with supporting material.

Estimated changes

added theorem div_pow_le
added theorem pos_div_pow_pos
added theorem hofer
added theorem geom_lt
added theorem sum_geometric_two_le
added theorem filter.Iio_mem_at_bot
added theorem filter.Ioi_mem_at_top
added theorem filter.inf_eq_bot_iff
added theorem filter.mem_at_bot
added theorem Iio_mem_nhds
added theorem Ioi_mem_nhds
added theorem Ioo_mem_nhds
added theorem disjoint_nhds_at_bot
added theorem disjoint_nhds_at_top
added theorem inf_nhds_at_bot
added theorem inf_nhds_at_top