Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-31 17:41 7e570ed1

View on Github →

chore(*): assorted small lemmas (#3644)

Estimated changes

Modified src/analysis/asymptotics.lean

added theorem asymptotics.is_o.trans_le

Modified src/analysis/normed_space/indicator_function.lean

added theorem nnnorm_indicator_eq_indicator_nnnorm

Modified src/data/real/ennreal.lean

added theorem ennreal.of_real_lt_top

Modified src/order/filter/basic.lean

added theorem filter.union_mem_sup

Modified src/order/liminf_limsup.lean

added theorem filter.is_bounded_under.mono

Modified src/topology/instances/ennreal.lean