Theorem liminfgf

Description: Closure of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypothesis	liminfgf.1	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
Assertion	liminfgf	⊢ 𝐺 : ℝ ⟶ ℝ*

Proof

Step	Hyp	Ref	Expression
1		liminfgf.1	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
2		inss2	⊢ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ*
3		infxrcl	⊢ ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* → inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* )
4	2 3	mp1i	⊢ ( 𝑘 ∈ ℝ → inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* )
5	1 4	fmpti	⊢ 𝐺 : ℝ ⟶ ℝ*