Theorem xrtgioo2

Description: The topology on the extended reals coincides with the standard topology on the reals, when restricted to RR . (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Assertion	xrtgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}ℝ$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}ℝ=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}ℝ$$
2	1	xrtgioo	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}ℝ$$