Database
BASIC TOPOLOGY
Topology
Separated spaces: T0, T1, T2 (Hausdorff) ...
resthaus
Metamath Proof Explorer
Description: A subspace of a Hausdorff topology is Hausdorff. (Contributed by Mario
Carneiro , 2-Mar-2015) (Proof shortened by Mario Carneiro , 25-Aug-2015)
Ref
Expression
Assertion
resthaus
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ Haus )
Proof
Step
Hyp
Ref
Expression
1
haustop
⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Top )
2
cnhaus
⊢ ( ( 𝐽 ∈ Haus ∧ ( I ↾ ( 𝐴 ∩ ∪ 𝐽 ) ) : ( 𝐴 ∩ ∪ 𝐽 ) –1-1 → ( 𝐴 ∩ ∪ 𝐽 ) ∧ ( I ↾ ( 𝐴 ∩ ∪ 𝐽 ) ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐽 ) ) → ( 𝐽 ↾t 𝐴 ) ∈ Haus )
3
1 2
resthauslem
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ Haus )