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

Metamath Proof Explorer

Theorem limsupgf

Description: Closure of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by Mario Carneiro, 7-May-2016)

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

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