Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-26 12:24 cde1bd87

View on Github →

Merge branch 'master' of https://github.com/leanprover/mathlib

Estimated changes

Modified topology/continuity.lean

added theorem is_open_prod

added theorem is_open_prod_iff

deleted theorem is_open_set_prod

Modified topology/real.lean

deleted theorem continuous_add_rat

deleted theorem continuous_add_real'

deleted theorem continuous_add_real

deleted theorem continuous_neg_rat

deleted theorem continuous_neg_real

deleted theorem continuous_sub_real

modified theorem exists_supremum_real

deleted theorem is_closed_ge

deleted theorem is_closed_le

deleted theorem is_closed_le_real

deleted theorem is_open_gt

deleted theorem is_open_lt

deleted theorem is_open_lt_real

deleted theorem tendsto_add_rat

deleted theorem tendsto_mul_rat

deleted theorem tendsto_neg_rat

Created topology/topological_structures.lean

added theorem continuous_add'

added theorem continuous_add

added theorem continuous_mul

added theorem continuous_neg'

added theorem continuous_neg

added theorem continuous_sub

added theorem dense_or_discrete

added theorem is_closed_le

added theorem is_open_lt

added theorem is_open_lt_fst_snd

added theorem order_separated

added theorem tendsto_add

added theorem tendsto_mul

added theorem tendsto_neg

added theorem tendsto_sub