Description: The topology of the complex numbers is Hausdorff. (Contributed by Mario Carneiro, 8-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | cnfldtopn.1 | ⊢ 𝐽 = ( TopOpen ‘ ℂfld ) | |
Assertion | cnfldhaus | ⊢ 𝐽 ∈ Haus |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnfldtopn.1 | ⊢ 𝐽 = ( TopOpen ‘ ℂfld ) | |
2 | cnxmet | ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) | |
3 | 1 | cnfldtopn | ⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) ) |
4 | 3 | methaus | ⊢ ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) → 𝐽 ∈ Haus ) |
5 | 2 4 | ax-mp | ⊢ 𝐽 ∈ Haus |