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

Metamath Proof Explorer

Theorem liminfresuz2

Description: If the domain of a function is a subset of the integers, the inferior limit doesn't change when the function is restricted to an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminfresuz2.1	$⊢ φ \to M \in ℤ$
	liminfresuz2.2	$⊢ Z = ℤ_{\geq M}$
	liminfresuz2.3	$⊢ φ \to F \in V$
	liminfresuz2.4	$⊢ φ \to dom F \subseteq ℤ$
Assertion	liminfresuz2	$⊢ φ \to lim inf ({F ↾}_{Z}) = lim inf (F)$

Proof

Step	Hyp	Ref	Expression
1		liminfresuz2.1	$⊢ φ \to M \in ℤ$
2		liminfresuz2.2	$⊢ Z = ℤ_{\geq M}$
3		liminfresuz2.3	$⊢ φ \to F \in V$
4		liminfresuz2.4	$⊢ φ \to dom F \subseteq ℤ$
5		dmresss	$⊢ dom ({F ↾}_{ℝ}) \subseteq dom F$
6	5	a1i	$⊢ φ \to dom ({F ↾}_{ℝ}) \subseteq dom F$
7	6 4	sstrd	$⊢ φ \to dom ({F ↾}_{ℝ}) \subseteq ℤ$
8	1 2 3 7	liminfresuz	$⊢ φ \to lim inf ({F ↾}_{Z}) = lim inf (F)$