Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-24 16:04 dc6b8e1c

View on Github →

feat(topology): add some lemmas (#9907)

  • From the sphere eversion project
  • Add compositional version continuous.fst of continuous_fst, compare measurable.fst.
  • Add comp_continuous_at_iff and comp_continuous_at_iff' for homeomorph (and for inducing).
  • Add some variants of these (requested by review).

Estimated changes

added theorem continuous.fst
added theorem continuous.snd
added theorem continuous_at.fst
added theorem continuous_at.snd
added theorem continuous_on.fst
added theorem continuous_on.snd