Description: If two sets are precisely separated by a continuous function, then they are separated by the continuous function. (Contributed by Zhi Wang, 9-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | seppsepf.1 | ||
Assertion | seppsepf |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | seppsepf.1 | ||
2 | eqimss | ||
3 | eqimss | ||
4 | 2 3 | anim12i | |
5 | 4 | reximi | |
6 | 1 5 | syl |