Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-07 20:38 ddeefb87

View on Github →

feat(topology/topological_structures,ennreal): show continuity of of_ennreal and of_real

Estimated changes

Modified data/set/basic.lean

added theorem set.image_inter_on

modified theorem set.mem_range

Modified order/filter.lean

added theorem filter.eq_of_map_eq_map_inj'

added theorem filter.le_of_map_le_map_inj'

modified theorem filter.map_binfi_eq

added theorem filter.map_inf'

added theorem filter.tendsto_principal

Modified order/lattice.lean

added theorem lattice.not_lt_bot

added theorem lattice.not_top_lt

Modified topology/ennreal.lean

added theorem ennreal.nhds_of_real_eq_map_of_real_nhds

added theorem ennreal.tendsto_of_ennreal

added theorem ennreal.tendsto_of_real

Modified topology/topological_space.lean

added theorem is_open_neg

Modified topology/topological_structures.lean

added theorem binfi_inf

added theorem is_closed_ge'

added theorem is_closed_le'

modified theorem is_open_gt'

modified theorem is_open_lt'

added theorem lt_min_iff

added theorem max_lt_iff

added theorem mem_nhds_lattice_unbounded

added theorem nhds_bot_orderable

added theorem nhds_eq_orderable

added theorem nhds_orderable_unbounded

added theorem nhds_top_orderable

added theorem tendsto_orderable

added theorem tendsto_orderable_unbounded