Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-11 13:56 b8904250

View on Github →

feat(topology/ennreal): ennreal forms a topological monoid

Estimated changes

Modified order/filter.lean

added theorem filter.tendsto_inf_left

Modified topology/ennreal.lean

added theorem ennreal.nhds_of_real_eq_map_of_real_nhds_nonneg

Modified topology/real.lean

deleted theorem ge_mem_nhds

deleted theorem gt_mem_nhds

deleted theorem le_mem_nhds

deleted theorem lt_mem_nhds

Modified topology/topological_structures.lean

added theorem ge_mem_nhds

added theorem gt_mem_nhds

added theorem le_mem_nhds

added theorem lt_mem_nhds