Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-14 07:28 21a71de1

View on Github →

chore(*): use notation instead of set.* (#14139)

Estimated changes

Modified src/computability/language.lean

Modified src/data/real/ereal.lean

modified def ereal.ne_top_bot_equiv_real

Modified src/group_theory/free_product.lean

Modified src/measure_theory/measure/measure_space.lean

Modified src/topology/instances/ereal.lean

modified theorem ereal.continuous_on_to_real

modified def ereal.ne_bot_top_homeomorph_real