Description: Alternate expression for the topology generated by a basis. Lemma 2.1 of Munkres p. 80. See also tgval and tgval2 . (Contributed by NM, 17-Jul-2006) (Revised by Mario Carneiro, 30-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | tgval3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eltg3 | |
|
2 | 1 | abbi2dv | |