This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database SUPPLEMENTARY MATERIAL (USERS' MATHBOXES) Mathbox for Glauco Siliprandi Limits Inferior limit (lim inf) 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 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
liminfresuz2.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
liminfresuz2.3 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
liminfresuz2.4 ⊢ ( 𝜑 → dom 𝐹 ⊆ ℤ )
Assertion
liminfresuz2 ⊢ ( 𝜑 → ( lim inf ‘ ( 𝐹 ↾ 𝑍 ) ) = ( lim inf ‘ 𝐹 ) )
Proof
Step
Hyp
Ref
Expression
1
liminfresuz2.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2
liminfresuz2.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3
liminfresuz2.3 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
4
liminfresuz2.4 ⊢ ( 𝜑 → dom 𝐹 ⊆ ℤ )
5
dmresss ⊢ dom ( 𝐹 ↾ ℝ ) ⊆ dom 𝐹
6
5
a1i ⊢ ( 𝜑 → dom ( 𝐹 ↾ ℝ ) ⊆ dom 𝐹 )
7
6 4
sstrd ⊢ ( 𝜑 → dom ( 𝐹 ↾ ℝ ) ⊆ ℤ )
8
1 2 3 7
liminfresuz ⊢ ( 𝜑 → ( lim inf ‘ ( 𝐹 ↾ 𝑍 ) ) = ( lim inf ‘ 𝐹 ) )