![]() |
Metamath
Proof Explorer Theorem List (p. 439 of 472) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-29746) |
![]() (29747-31269) |
![]() (31270-47184) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | limcperiod 43801* | If 𝐹 is a periodic function with period 𝑇, the limit doesn't change if we shift the limiting point by 𝑇. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐴 ⊆ dom 𝐹) & ⊢ (𝜑 → 𝑇 ∈ ℂ) & ⊢ 𝐵 = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇)} & ⊢ (𝜑 → 𝐵 ⊆ dom 𝐹) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦)) & ⊢ (𝜑 → 𝐶 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐷)) ⇒ ⊢ (𝜑 → 𝐶 ∈ ((𝐹 ↾ 𝐵) limℂ (𝐷 + 𝑇))) | ||
Theorem | limcrecl 43802 | If 𝐹 is a real-valued function, 𝐵 is a limit point of its domain, and the limit of 𝐹 at 𝐵 exists, then this limit is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ((limPt‘(TopOpen‘ℂfld))‘𝐴)) & ⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵)) ⇒ ⊢ (𝜑 → 𝐿 ∈ ℝ) | ||
Theorem | sumnnodd 43803* | A series indexed by ℕ with only odd terms. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ ∧ (𝑘 / 2) ∈ ℕ) → (𝐹‘𝑘) = 0) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝐵) ⇒ ⊢ (𝜑 → (seq1( + , (𝑘 ∈ ℕ ↦ (𝐹‘((2 · 𝑘) − 1)))) ⇝ 𝐵 ∧ Σ𝑘 ∈ ℕ (𝐹‘𝑘) = Σ𝑘 ∈ ℕ (𝐹‘((2 · 𝑘) − 1)))) | ||
Theorem | lptioo2 43804 | The upper bound of an open interval is a limit point of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵))) | ||
Theorem | lptioo1 43805 | The lower bound of an open interval is a limit point of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵))) | ||
Theorem | elprn1 43806 | A member of an unordered pair that is not the "first", must be the "second". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐴 ≠ 𝐵) → 𝐴 = 𝐶) | ||
Theorem | elprn2 43807 | A member of an unordered pair that is not the "second", must be the "first". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐴 ≠ 𝐶) → 𝐴 = 𝐵) | ||
Theorem | limcmptdm 43808* | The domain of a maps-to function with a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐷)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ ℂ) | ||
Theorem | clim2f 43809* | Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴, with more general quantifier restrictions than clim 15368. Similar to clim2 15378, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥)))) | ||
Theorem | limcicciooub 43810 | The limit of a function at the upper bound of a closed interval only depends on the values in the inner open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) ⇒ ⊢ (𝜑 → ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐵) = (𝐹 limℂ 𝐵)) | ||
Theorem | ltmod 43811 | A sufficient condition for a "less than" relationship for the mod operator. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ((𝐴 − (𝐴 mod 𝐵))[,)𝐴)) ⇒ ⊢ (𝜑 → (𝐶 mod 𝐵) < (𝐴 mod 𝐵)) | ||
Theorem | islpcn 43812* | A characterization for a limit point for the standard topology on the complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝑃 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑃 ∈ ((limPt‘(TopOpen‘ℂfld))‘𝑆) ↔ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒)) | ||
Theorem | lptre2pt 43813* | If a set in the real line has a limit point than it contains two distinct points that are closer than a given distance. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → ((limPt‘𝐽)‘𝐴) ≠ ∅) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 ∧ (abs‘(𝑥 − 𝑦)) < 𝐸)) | ||
Theorem | limsupre 43814* | If a sequence is bounded, then the limsup is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 13-Sep-2020.) |
⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ (𝜑 → sup(𝐵, ℝ*, < ) = +∞) & ⊢ (𝜑 → 𝐹:𝐵⟶ℝ) & ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ⇒ ⊢ (𝜑 → (lim sup‘𝐹) ∈ ℝ) | ||
Theorem | limcresiooub 43815 | The left limit doesn't change if the function is restricted to a smaller open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 < 𝐶) & ⊢ (𝜑 → (𝐵(,)𝐶) ⊆ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ ℝ*) & ⊢ (𝜑 → 𝐷 ≤ 𝐵) ⇒ ⊢ (𝜑 → ((𝐹 ↾ (𝐵(,)𝐶)) limℂ 𝐶) = ((𝐹 ↾ (𝐷(,)𝐶)) limℂ 𝐶)) | ||
Theorem | limcresioolb 43816 | The right limit doesn't change if the function is restricted to a smaller open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 < 𝐶) & ⊢ (𝜑 → (𝐵(,)𝐶) ⊆ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ≤ 𝐷) ⇒ ⊢ (𝜑 → ((𝐹 ↾ (𝐵(,)𝐶)) limℂ 𝐵) = ((𝐹 ↾ (𝐵(,)𝐷)) limℂ 𝐵)) | ||
Theorem | limcleqr 43817 | If the left and the right limits are equal, the limit of the function exits and the three limits coincide. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵)) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵)) & ⊢ (𝜑 → 𝐿 = 𝑅) ⇒ ⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵)) | ||
Theorem | lptioo2cn 43818 | The upper bound of an open interval is a limit point of the interval, wirth respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵))) | ||
Theorem | lptioo1cn 43819 | The lower bound of an open interval is a limit point of the interval, wirth respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ ((limPt‘𝐽)‘(𝐴(,)𝐵))) | ||
Theorem | neglimc 43820* | Limit of the negative function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ -𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐷)) ⇒ ⊢ (𝜑 → -𝐶 ∈ (𝐺 limℂ 𝐷)) | ||
Theorem | addlimc 43821* | Sum of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐸 ∈ (𝐹 limℂ 𝐷)) & ⊢ (𝜑 → 𝐼 ∈ (𝐺 limℂ 𝐷)) ⇒ ⊢ (𝜑 → (𝐸 + 𝐼) ∈ (𝐻 limℂ 𝐷)) | ||
Theorem | 0ellimcdiv 43822* | If the numerator converges to 0 and the denominator converges to a nonzero number, then the fraction converges to 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (ℂ ∖ {0})) & ⊢ (𝜑 → 0 ∈ (𝐹 limℂ 𝐸)) & ⊢ (𝜑 → 𝐷 ∈ (𝐺 limℂ 𝐸)) & ⊢ (𝜑 → 𝐷 ≠ 0) ⇒ ⊢ (𝜑 → 0 ∈ (𝐻 limℂ 𝐸)) | ||
Theorem | clim2cf 43823* | Express the predicate 𝐹 converges to 𝐴. Similar to clim2 15378, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐵 − 𝐴)) < 𝑥)) | ||
Theorem | limclner 43824 | For a limit point, both from the left and from the right, of the domain, the limit of the function exits only if the left and the right limits are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵)))) & ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞)))) & ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵)) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵)) & ⊢ (𝜑 → 𝐿 ≠ 𝑅) ⇒ ⊢ (𝜑 → (𝐹 limℂ 𝐵) = ∅) | ||
Theorem | sublimc 43825* | Subtraction of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐸 ∈ (𝐹 limℂ 𝐷)) & ⊢ (𝜑 → 𝐼 ∈ (𝐺 limℂ 𝐷)) ⇒ ⊢ (𝜑 → (𝐸 − 𝐼) ∈ (𝐻 limℂ 𝐷)) | ||
Theorem | reclimc 43826* | Limit of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (ℂ ∖ {0})) & ⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐷)) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → (1 / 𝐶) ∈ (𝐺 limℂ 𝐷)) | ||
Theorem | clim0cf 43827* | Express the predicate 𝐹 converges to 0. Similar to clim 15368, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘𝐵) < 𝑥)) | ||
Theorem | limclr 43828 | For a limit point, both from the left and from the right, of the domain, the limit of the function exits only if the left and the right limits are equal. In this case, the three limits coincide. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (-∞(,)𝐵)))) & ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐽)‘(𝐴 ∩ (𝐵(,)+∞)))) & ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝐵)) limℂ 𝐵)) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐵(,)+∞)) limℂ 𝐵)) ⇒ ⊢ (𝜑 → (((𝐹 limℂ 𝐵) ≠ ∅ ↔ 𝐿 = 𝑅) ∧ (𝐿 = 𝑅 → 𝐿 ∈ (𝐹 limℂ 𝐵)))) | ||
Theorem | divlimc 43829* | Limit of the quotient of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (ℂ ∖ {0})) & ⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝐷)) & ⊢ (𝜑 → 𝑌 ∈ (𝐺 limℂ 𝐷)) & ⊢ (𝜑 → 𝑌 ≠ 0) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → (𝑋 / 𝑌) ∈ (𝐻 limℂ 𝐷)) | ||
Theorem | expfac 43830* | Factorial grows faster than exponential. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ⇝ 0) | ||
Theorem | climconstmpt 43831* | A constant sequence converges to its value. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐴) | ||
Theorem | climresmpt 43832* | A function restricted to upper integers converges iff the original function converges. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐹 = (𝑥 ∈ 𝑍 ↦ 𝐴) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ 𝐺 = (𝑥 ∈ (ℤ≥‘𝑁) ↦ 𝐴) ⇒ ⊢ (𝜑 → (𝐺 ⇝ 𝐵 ↔ 𝐹 ⇝ 𝐵)) | ||
Theorem | climsubmpt 43833* | Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐶) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐷) ⇒ ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) ⇝ (𝐶 − 𝐷)) | ||
Theorem | climsubc2mpt 43834* | Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) ⇝ (𝐶 − 𝐵)) | ||
Theorem | climsubc1mpt 43835* | Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐶) ⇒ ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) ⇝ (𝐴 − 𝐶)) | ||
Theorem | fnlimfv 43836* | The value of the limit function 𝐺 at any point of its domain 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐷 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝐺‘𝑋) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)))) | ||
Theorem | climreclf 43837* | The limit of a convergent real sequence is real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | climeldmeq 43838* | Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ )) | ||
Theorem | climf2 43839* | Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴. Similar to clim 15368, but without the disjoint var constraint 𝜑𝑘 and 𝐹𝑘. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝐹‘𝑘) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥)))) | ||
Theorem | fnlimcnv 43840* | The sequence of function values converges to the value of the limit function 𝐺 at any point of its domain 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐹 & ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)) ⇝ (𝐺‘𝑋)) | ||
Theorem | climeldmeqmpt 43841* | Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑅) & ⊢ (𝜑 → 𝑍 ⊆ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝑍 ⊆ 𝐶) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐷 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∈ dom ⇝ ↔ (𝑘 ∈ 𝐶 ↦ 𝐷) ∈ dom ⇝ )) | ||
Theorem | climfveq 43842* | Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → ( ⇝ ‘𝐹) = ( ⇝ ‘𝐺)) | ||
Theorem | clim2f2 43843* | Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴, with more general quantifier restrictions than clim 15368. Similar to clim2 15378, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥)))) | ||
Theorem | climfveqmpt 43844* | Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑅) & ⊢ (𝜑 → 𝑍 ⊆ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝑍 ⊆ 𝐶) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐷 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ( ⇝ ‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = ( ⇝ ‘(𝑘 ∈ 𝐶 ↦ 𝐷))) | ||
Theorem | climd 43845* | Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ (𝜑 → 𝑋 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑋)) | ||
Theorem | clim2d 43846* | The limit of complex number sequence 𝐹 is eventually approximated. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ (𝜑 → 𝑋 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑋)) | ||
Theorem | fnlimfvre 43847* | The limit function of real functions, applied to elements in its domain, evaluates to Real values. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑚𝜑 & ⊢ Ⅎ𝑚𝐹 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) & ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } & ⊢ (𝜑 → 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋))) ∈ ℝ) | ||
Theorem | allbutfifvre 43848* | Given a sequence of real-valued functions, and 𝑋 that belongs to all but finitely many domains, then its function value is ultimately a real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑚𝜑 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) & ⊢ 𝐷 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)((𝐹‘𝑚)‘𝑋) ∈ ℝ) | ||
Theorem | climleltrp 43849* | The limit of complex number sequence 𝐹 is eventually approximated. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝑋 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋))) | ||
Theorem | fnlimfvre2 43850* | The limit function of real functions, applied to elements in its domain, evaluates to Real values. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑚𝜑 & ⊢ Ⅎ𝑚𝐹 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) & ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝐺‘𝑋) ∈ ℝ) | ||
Theorem | fnlimf 43851* | The limit function of real functions, is a real-valued function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑚𝜑 & ⊢ Ⅎ𝑚𝐹 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) & ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) ⇒ ⊢ (𝜑 → 𝐺:𝐷⟶ℝ) | ||
Theorem | fnlimabslt 43852* | A sequence of function values, approximates the corresponding limit function value, all but finitely many times. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑚𝜑 & ⊢ Ⅎ𝑚𝐹 & ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) & ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑌 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)(((𝐹‘𝑚)‘𝑋) ∈ ℝ ∧ (abs‘(((𝐹‘𝑚)‘𝑋) − (𝐺‘𝑋))) < 𝑌)) | ||
Theorem | climfveqf 43853* | Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ Ⅎ𝑘𝐺 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → ( ⇝ ‘𝐹) = ( ⇝ ‘𝐺)) | ||
Theorem | climmptf 43854* | Exhibit a function 𝐺 with the same convergence properties as the not-quite-function 𝐹. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐺 = (𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴)) | ||
Theorem | climfveqmpt3 43855* | Two functions that are eventually equal to one another have the same limit. TODO: this is more general than climfveqmpt 43844 and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ (𝜑 → 𝑍 ⊆ 𝐴) & ⊢ (𝜑 → 𝑍 ⊆ 𝐶) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ 𝑈) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ( ⇝ ‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = ( ⇝ ‘(𝑘 ∈ 𝐶 ↦ 𝐷))) | ||
Theorem | climeldmeqf 43856* | Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ Ⅎ𝑘𝐺 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom ⇝ ↔ 𝐺 ∈ dom ⇝ )) | ||
Theorem | climreclmpt 43857* | The limit of B convergent real sequence is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ∈ ℝ) | ||
Theorem | limsupref 43858* | If a sequence is bounded, then the limsup is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝐹 & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ⇒ ⊢ (𝜑 → (lim sup‘𝐹) ∈ ℝ) | ||
Theorem | limsupbnd1f 43859* | If a sequence is eventually at most 𝐴, then the limsup is also at most 𝐴. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝐹 & ⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐵⟶ℝ*) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴)) ⇒ ⊢ (𝜑 → (lim sup‘𝐹) ≤ 𝐴) | ||
Theorem | climbddf 43860* | A converging sequence of complex numbers is bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ∧ ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ∈ ℂ) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ≤ 𝑥) | ||
Theorem | climeqf 43861* | Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ Ⅎ𝑘𝐺 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴)) | ||
Theorem | climeldmeqmpt3 43862* | Two functions that are eventually equal, either both are convergent or both are divergent. TODO: this is more general than climeldmeqmpt 43841 and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ (𝜑 → 𝑍 ⊆ 𝐴) & ⊢ (𝜑 → 𝑍 ⊆ 𝐶) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ 𝑈) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∈ dom ⇝ ↔ (𝑘 ∈ 𝐶 ↦ 𝐷) ∈ dom ⇝ )) | ||
Theorem | limsupcld 43863 | Closure of the superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) ⇒ ⊢ (𝜑 → (lim sup‘𝐹) ∈ ℝ*) | ||
Theorem | climfv 43864 | The limit of a convergent sequence, expressed as the function value of the convergence relation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐹 ⇝ 𝐴 → 𝐴 = ( ⇝ ‘𝐹)) | ||
Theorem | limsupval3 43865* | The superior limit of an infinite sequence 𝐹 of extended real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) & ⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup((𝐹 “ (𝑘[,)+∞)), ℝ*, < )) ⇒ ⊢ (𝜑 → (lim sup‘𝐹) = inf(ran 𝐺, ℝ*, < )) | ||
Theorem | climfveqmpt2 43866* | Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑍 ⊆ 𝐴) & ⊢ (𝜑 → 𝑍 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → ( ⇝ ‘(𝑘 ∈ 𝐴 ↦ 𝐶)) = ( ⇝ ‘(𝑘 ∈ 𝐵 ↦ 𝐶))) | ||
Theorem | limsup0 43867 | The superior limit of the empty set. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (lim sup‘∅) = -∞ | ||
Theorem | climeldmeqmpt2 43868* | Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ⊆ 𝐴) & ⊢ (𝜑 → 𝑍 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐶) ∈ dom ⇝ ↔ (𝑘 ∈ 𝐵 ↦ 𝐶) ∈ dom ⇝ )) | ||
Theorem | limsupresre 43869 | The supremum limit of a function only depends on the real part of its domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) ⇒ ⊢ (𝜑 → (lim sup‘(𝐹 ↾ ℝ)) = (lim sup‘𝐹)) | ||
Theorem | climeqmpt 43870* | Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑍 ⊆ 𝐴) & ⊢ (𝜑 → 𝑍 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ⇝ 𝐷 ↔ (𝑥 ∈ 𝐵 ↦ 𝐶) ⇝ 𝐷)) | ||
Theorem | climfvd 43871 | The limit of a convergent sequence, expressed as the function value of the convergence relation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹 ⇝ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = ( ⇝ ‘𝐹)) | ||
Theorem | limsuplesup 43872 | An upper bound for the superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐾 ∈ ℝ) ⇒ ⊢ (𝜑 → (lim sup‘𝐹) ≤ sup(((𝐹 “ (𝐾[,)+∞)) ∩ ℝ*), ℝ*, < )) | ||
Theorem | limsupresico 43873 | The superior limit doesn't change when a function is restricted to the upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ 𝑍 = (𝑀[,)+∞) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) ⇒ ⊢ (𝜑 → (lim sup‘(𝐹 ↾ 𝑍)) = (lim sup‘𝐹)) | ||
Theorem | limsuppnfdlem 43874* | If the restriction of a function to every upper interval is unbounded above, its lim sup is +∞. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) & ⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) ⇒ ⊢ (𝜑 → (lim sup‘𝐹) = +∞) | ||
Theorem | limsuppnfd 43875* | If the restriction of a function to every upper interval is unbounded above, its lim sup is +∞. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝐹 & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) ⇒ ⊢ (𝜑 → (lim sup‘𝐹) = +∞) | ||
Theorem | limsupresuz 43876 | If the real part of the domain of a function is a subset of the integers, the superior limit doesn't change when the function is restricted to an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → dom (𝐹 ↾ ℝ) ⊆ ℤ) ⇒ ⊢ (𝜑 → (lim sup‘(𝐹 ↾ 𝑍)) = (lim sup‘𝐹)) | ||
Theorem | limsupub 43877* | If the limsup is not +∞, then the function is eventually bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝜑 & ⊢ Ⅎ𝑗𝐹 & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) & ⊢ (𝜑 → (lim sup‘𝐹) ≠ +∞) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) | ||
Theorem | limsupres 43878 | The superior limit of a restriction is less than or equal to the original superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) ⇒ ⊢ (𝜑 → (lim sup‘(𝐹 ↾ 𝐶)) ≤ (lim sup‘𝐹)) | ||
Theorem | climinf2lem 43879* | A convergent, nonincreasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 𝑥 ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → 𝐹 ⇝ inf(ran 𝐹, ℝ*, < )) | ||
Theorem | climinf2 43880* | A convergent, nonincreasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 𝑥 ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → 𝐹 ⇝ inf(ran 𝐹, ℝ*, < )) | ||
Theorem | limsupvaluz 43881* | The superior limit, when the domain of the function is a set of upper integers (the first condition is needed, otherwise the l.h.s. would be -∞ and the r.h.s. would be +∞). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) ⇒ ⊢ (𝜑 → (lim sup‘𝐹) = inf(ran (𝑘 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ≥‘𝑘)), ℝ*, < )), ℝ*, < )) | ||
Theorem | limsupresuz2 43882 | If the domain of a function is a subset of the integers, the superior limit doesn't change when the function is restricted to an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → dom 𝐹 ⊆ ℤ) ⇒ ⊢ (𝜑 → (lim sup‘(𝐹 ↾ 𝑍)) = (lim sup‘𝐹)) | ||
Theorem | limsuppnflem 43883* | If the restriction of a function to every upper interval is unbounded above, its lim sup is +∞. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝐹 & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) ⇒ ⊢ (𝜑 → ((lim sup‘𝐹) = +∞ ↔ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)))) | ||
Theorem | limsuppnf 43884* | If the restriction of a function to every upper interval is unbounded above, its lim sup is +∞. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝐹 & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) ⇒ ⊢ (𝜑 → ((lim sup‘𝐹) = +∞ ↔ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)))) | ||
Theorem | limsupubuzlem 43885* | If the limsup is not +∞, then the function is bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝜑 & ⊢ Ⅎ𝑗𝑋 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝐾 ∈ ℝ) & ⊢ (𝜑 → ∀𝑗 ∈ 𝑍 (𝐾 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑌)) & ⊢ 𝑁 = if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾)) & ⊢ 𝑊 = sup(ran (𝑗 ∈ (𝑀...𝑁) ↦ (𝐹‘𝑗)), ℝ, < ) & ⊢ 𝑋 = if(𝑊 ≤ 𝑌, 𝑌, 𝑊) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑥) | ||
Theorem | limsupubuz 43886* | For a real-valued function on a set of upper integers, if the superior limit is not +∞, then the function is bounded above. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ) & ⊢ (𝜑 → (lim sup‘𝐹) ≠ +∞) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑥) | ||
Theorem | climinf2mpt 43887* | A bounded below, monotonic nonincreasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑗𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝑘 = 𝑗 → 𝐵 = 𝐶) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍 ∧ 𝑗 = (𝑘 + 1)) → 𝐶 ≤ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐵) ⇝ inf(ran (𝑘 ∈ 𝑍 ↦ 𝐵), ℝ*, < )) | ||
Theorem | climinfmpt 43888* | A bounded below, monotonic nonincreasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑗𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝑘 = 𝑗 → 𝐵 = 𝐶) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍 ∧ 𝑗 = (𝑘 + 1)) → 𝐶 ≤ 𝐵) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 𝑥 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐵) ⇝ inf(ran (𝑘 ∈ 𝑍 ↦ 𝐵), ℝ*, < )) | ||
Theorem | climinf3 43889* | A convergent, nonincreasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) & ⊢ (𝜑 → 𝐹 ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → 𝐹 ⇝ inf(ran 𝐹, ℝ*, < )) | ||
Theorem | limsupvaluzmpt 43890* | The superior limit, when the domain of the function is a set of upper integers (the first condition is needed, otherwise the l.h.s. would be -∞ and the r.h.s. would be +∞). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (lim sup‘(𝑗 ∈ 𝑍 ↦ 𝐵)) = inf(ran (𝑘 ∈ 𝑍 ↦ sup(ran (𝑗 ∈ (ℤ≥‘𝑘) ↦ 𝐵), ℝ*, < )), ℝ*, < )) | ||
Theorem | limsupequzmpt2 43891* | Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝜑 & ⊢ Ⅎ𝑗𝐴 & ⊢ Ⅎ𝑗𝐵 & ⊢ 𝐴 = (ℤ≥‘𝑀) & ⊢ 𝐵 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐾 ∈ 𝐴) & ⊢ (𝜑 → 𝐾 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → (lim sup‘(𝑗 ∈ 𝐴 ↦ 𝐶)) = (lim sup‘(𝑗 ∈ 𝐵 ↦ 𝐶))) | ||
Theorem | limsupubuzmpt 43892* | If the limsup is not +∞, then the function is eventually bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝜑 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (lim sup‘(𝑗 ∈ 𝑍 ↦ 𝐵)) ≠ +∞) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 𝐵 ≤ 𝑥) | ||
Theorem | limsupmnflem 43893* | The superior limit of a function is -∞ if and only if every real number is the upper bound of the restriction of the function to an upper interval of real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) & ⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup((𝐹 “ (𝑘[,)+∞)), ℝ*, < )) ⇒ ⊢ (𝜑 → ((lim sup‘𝐹) = -∞ ↔ ∀𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))) | ||
Theorem | limsupmnf 43894* | The superior limit of a function is -∞ if and only if every real number is the upper bound of the restriction of the function to an upper interval of real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝐹 & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) ⇒ ⊢ (𝜑 → ((lim sup‘𝐹) = -∞ ↔ ∀𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))) | ||
Theorem | limsupequzlem 43895* | Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 Fn (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐺 Fn (ℤ≥‘𝑁)) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → (lim sup‘𝐹) = (lim sup‘𝐺)) | ||
Theorem | limsupequz 43896* | Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ Ⅎ𝑘𝐺 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 Fn (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐺 Fn (ℤ≥‘𝑁)) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝐾)) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → (lim sup‘𝐹) = (lim sup‘𝐺)) | ||
Theorem | limsupre2lem 43897* | Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is smaller than the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually larger than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝐹 & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) ⇒ ⊢ (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔ (∃𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗)) ∧ ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) < 𝑥)))) | ||
Theorem | limsupre2 43898* | Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is smaller than the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually larger than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝐹 & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) ⇒ ⊢ (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔ (∃𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗)) ∧ ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) < 𝑥)))) | ||
Theorem | limsupmnfuzlem 43899* | The superior limit of a function is -∞ if and only if every real number is the upper bound of the restriction of the function to a set of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) ⇒ ⊢ (𝜑 → ((lim sup‘𝐹) = -∞ ↔ ∀𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥)) | ||
Theorem | limsupmnfuz 43900* | The superior limit of a function is -∞ if and only if every real number is the upper bound of the restriction of the function to a set of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) ⇒ ⊢ (𝜑 → ((lim sup‘𝐹) = -∞ ↔ ∀𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |