mathlib
8acd296e - chore(topology/path_connected): move `proj_Icc` to a separate file (#5120)

Commit

5 years ago

chore(topology/path_connected): move `proj_Icc` to a separate file (#5120) Also use `min` and `max` in the definition to make, e.g., the proof of the continuity trivial.

Author

urkud

Parents

238c58c3

mathlib 8acd296e - chore(topology/path_connected): move `proj_Icc` to a separate file (#5120)

mathlib
8acd296e - chore(topology/path_connected): move `proj_Icc` to a separate file (#5120)