Description: A subspace of a T_0 topology is T_0. (Contributed by Mario Carneiro, 25-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | restt0 | ⊢ ( ( 𝐽 ∈ Kol2 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ Kol2 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | t0top | ⊢ ( 𝐽 ∈ Kol2 → 𝐽 ∈ Top ) | |
2 | cnt0 | ⊢ ( ( 𝐽 ∈ Kol2 ∧ ( I ↾ ( 𝐴 ∩ ∪ 𝐽 ) ) : ( 𝐴 ∩ ∪ 𝐽 ) –1-1→ ( 𝐴 ∩ ∪ 𝐽 ) ∧ ( I ↾ ( 𝐴 ∩ ∪ 𝐽 ) ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐽 ) ) → ( 𝐽 ↾t 𝐴 ) ∈ Kol2 ) | |
3 | 1 2 | resthauslem | ⊢ ( ( 𝐽 ∈ Kol2 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ Kol2 ) |