Theorem liminfresre

Description: The inferior limit of a function only depends on the real part of its domain. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypothesis	liminfresre.1	$$⊢\phi \to F\in V$$
Assertion	liminfresre	$$⊢\phi \to \mathrm{lim\; inf}\left({F\upharpoonright }_{ℝ}\right)=\mathrm{lim\; inf}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		liminfresre.1	$$⊢\phi \to F\in V$$
2		rge0ssre	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq ℝ$$
3	2	resabs1i	$$⊢{\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\left[0,\mathrm{+\infty }\right)}={F\upharpoonright }_{\left[0,\mathrm{+\infty }\right)}$$
4	3	fveq2i	$$⊢\mathrm{lim\; inf}\left({\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\left[0,\mathrm{+\infty }\right)}\right)=\mathrm{lim\; inf}\left({F\upharpoonright }_{\left[0,\mathrm{+\infty }\right)}\right)$$
5	4	a1i	$$⊢\phi \to \mathrm{lim\; inf}\left({\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\left[0,\mathrm{+\infty }\right)}\right)=\mathrm{lim\; inf}\left({F\upharpoonright }_{\left[0,\mathrm{+\infty }\right)}\right)$$
6		0red	$$⊢\phi \to 0\in ℝ$$
7		eqid	$$⊢\left[0,\mathrm{+\infty }\right)=\left[0,\mathrm{+\infty }\right)$$
8	1	resexd	$$⊢\phi \to {F\upharpoonright }_{ℝ}\in \mathrm{V}$$
9	6 7 8	liminfresico	$$⊢\phi \to \mathrm{lim\; inf}\left({\left({F\upharpoonright }_{ℝ}\right)\upharpoonright }_{\left[0,\mathrm{+\infty }\right)}\right)=\mathrm{lim\; inf}\left({F\upharpoonright }_{ℝ}\right)$$
10	6 7 1	liminfresico	$$⊢\phi \to \mathrm{lim\; inf}\left({F\upharpoonright }_{\left[0,\mathrm{+\infty }\right)}\right)=\mathrm{lim\; inf}\left(F\right)$$
11	5 9 10	3eqtr3d	$$⊢\phi \to \mathrm{lim\; inf}\left({F\upharpoonright }_{ℝ}\right)=\mathrm{lim\; inf}\left(F\right)$$