Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-06 19:31 32f3f452

View on Github →

feat(topology): restructure order topologies; (start) proof that ennreal is a topological monoid

Estimated changes

Modified algebra/group.lean

added theorem abs_lt_iff

Modified topology/ennreal.lean

added theorem ennreal.continuous_of_real

added theorem ennreal.inv_infty

added theorem ennreal.inv_inv

added theorem ennreal.inv_of_real

added theorem ennreal.inv_zero

added theorem ennreal.not_lt_zero

added theorem ennreal.of_real_lt_of_real_iff_cases

added theorem ennreal.of_real_of_nonpos

added theorem ennreal.of_real_of_not_nonneg

added theorem ennreal.one_le_of_real_iff

added theorem ennreal.zero_lt_of_real_iff

added theorem inv_inv'

added theorem inv_pos

Modified topology/real.lean

deleted theorem is_closed_imp

added theorem lt_sub_iff

added theorem nhds_eq_real

added theorem orderable_topology_of_nhds_abs

added theorem sub_lt_iff

Modified topology/topological_space.lean

modified theorem closure_diff

added theorem is_closed_imp

added theorem is_open_and

added theorem is_open_const

added theorem mem_of_closed_of_tendsto

Modified topology/topological_structures.lean

added theorem is_open_gt'

added theorem is_open_iff_generate_intervals

added theorem is_open_lt'

deleted theorem is_open_lt_fst_snd

added theorem le_of_tendsto

Modified topology/uniform_space.lean

added theorem nhds_eq_vmap_uniformity