This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem liminfgf

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

		Ref	Expression
	Hypothesis	liminfgf.1	$⊢ G = (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
	Assertion	liminfgf	$⊢ G : ℝ ⟶ ℝ^{*}$

Step	Hyp	Ref	Expression
1		liminfgf.1	$⊢ G = (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
2		inss2	$⊢ F [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
3		infxrcl	$⊢ F [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{} \to inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
4	2 3	mp1i	$⊢ k \in ℝ \to inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
5	1 4	fmpti	$⊢ G : ℝ ⟶ ℝ^{*}$