Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-28 19:28 e7b2a0f7

View on Github →

style(analysis): renames the topology directory to analysis and introduced topology and measure_theory subdirectories

Estimated changes

Renamed topology/ennreal.lean to analysis/ennreal.lean

Renamed topology/limits.lean to analysis/limits.lean

added theorem has_sum_of_absolute_convergence

added theorem is_sum_iff_tendsto_nat_of_nonneg

Renamed topology/borel_space.lean to analysis/measure_theory/borel_space.lean

Renamed topology/lebesgue_measure.lean to analysis/measure_theory/lebesgue_measure.lean

Renamed topology/measurable_space.lean to analysis/measure_theory/measurable_space.lean

Renamed topology/measure.lean to analysis/measure_theory/measure_space.lean

Renamed topology/outer_measure.lean to analysis/measure_theory/outer_measure.lean

Renamed topology/metric_space.lean to analysis/metric_space.lean

Renamed topology/of_nat.lean to analysis/of_nat.lean

Renamed topology/real.lean to analysis/real.lean

Renamed topology/continuity.lean to analysis/topology/continuity.lean

Renamed topology/infinite_sum.lean to analysis/topology/infinite_sum.lean

deleted theorem has_sum_of_absolute_convergence

deleted theorem is_sum_iff_tendsto_nat_of_nonneg

Renamed topology/topological_space.lean to analysis/topology/topological_space.lean

Renamed topology/topological_structures.lean to analysis/topology/topological_structures.lean

Renamed topology/uniform_space.lean to analysis/topology/uniform_space.lean