Home | Metamath
Proof Explorer Theorem List (p. 419 of 449) | < 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: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lptre2pt 41801* | 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 41802* | 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 41803 | 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 41804 | 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 41805 | 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 41806 | 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 41807 | 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 41808* | Limit of the negative function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ -𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐷)) ⇒ ⊢ (𝜑 → -𝐶 ∈ (𝐺 limℂ 𝐷)) | ||
Theorem | addlimc 41809* | Sum of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐸 ∈ (𝐹 limℂ 𝐷)) & ⊢ (𝜑 → 𝐼 ∈ (𝐺 limℂ 𝐷)) ⇒ ⊢ (𝜑 → (𝐸 + 𝐼) ∈ (𝐻 limℂ 𝐷)) | ||
Theorem | 0ellimcdiv 41810* | 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 41811* | Express the predicate 𝐹 converges to 𝐴. Similar to clim2 14851, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐵 − 𝐴)) < 𝑥)) | ||
Theorem | limclner 41812 | 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 41813* | Subtraction of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐸 ∈ (𝐹 limℂ 𝐷)) & ⊢ (𝜑 → 𝐼 ∈ (𝐺 limℂ 𝐷)) ⇒ ⊢ (𝜑 → (𝐸 − 𝐼) ∈ (𝐻 limℂ 𝐷)) | ||
Theorem | reclimc 41814* | Limit of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (ℂ ∖ {0})) & ⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐷)) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → (1 / 𝐶) ∈ (𝐺 limℂ 𝐷)) | ||
Theorem | clim0cf 41815* | Express the predicate 𝐹 converges to 0. Similar to clim 14841, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘𝐵) < 𝑥)) | ||
Theorem | limclr 41816 | 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 41817* | Limit of the quotient of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (ℂ ∖ {0})) & ⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝐷)) & ⊢ (𝜑 → 𝑌 ∈ (𝐺 limℂ 𝐷)) & ⊢ (𝜑 → 𝑌 ≠ 0) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → (𝑋 / 𝑌) ∈ (𝐻 limℂ 𝐷)) | ||
Theorem | expfac 41818* | Factorial grows faster than exponential. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ⇝ 0) | ||
Theorem | climconstmpt 41819* | A constant sequence converges to its value. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐴) | ||
Theorem | climresmpt 41820* | A function restricted to upper integers converges iff the original function converges. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐹 = (𝑥 ∈ 𝑍 ↦ 𝐴) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ 𝐺 = (𝑥 ∈ (ℤ≥‘𝑁) ↦ 𝐴) ⇒ ⊢ (𝜑 → (𝐺 ⇝ 𝐵 ↔ 𝐹 ⇝ 𝐵)) | ||
Theorem | climsubmpt 41821* | Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐶) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐷) ⇒ ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) ⇝ (𝐶 − 𝐷)) | ||
Theorem | climsubc2mpt 41822* | Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) ⇝ (𝐶 − 𝐵)) | ||
Theorem | climsubc1mpt 41823* | Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐶) ⇒ ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝐴 − 𝐵)) ⇝ (𝐴 − 𝐶)) | ||
Theorem | fnlimfv 41824* | The value of the limit function 𝐺 at any point of its domain 𝐷. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐷 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝐺‘𝑋) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑋)))) | ||
Theorem | climreclf 41825* | The limit of a convergent real sequence is real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | climeldmeq 41826* | 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 41827* | Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴. Similar to clim 14841, but without the disjoint var constraint 𝜑𝑘 and 𝐹𝑘. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝐹‘𝑘) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥)))) | ||
Theorem | fnlimcnv 41828* | 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 41829* | 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 41830* | Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → ( ⇝ ‘𝐹) = ( ⇝ ‘𝐺)) | ||
Theorem | clim2f2 41831* | Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴, with more general quantifier restrictions than clim 14841. Similar to clim2 14851, but without the disjoint var constraint 𝐹𝑘. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥)))) | ||
Theorem | climfveqmpt 41832* | Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑅) & ⊢ (𝜑 → 𝑍 ⊆ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝑍 ⊆ 𝐶) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐷 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ( ⇝ ‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = ( ⇝ ‘(𝑘 ∈ 𝐶 ↦ 𝐷))) | ||
Theorem | climd 41833* | Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ (𝜑 → 𝑋 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑋)) | ||
Theorem | clim2d 41834* | The limit of complex number sequence 𝐹 is eventually approximated. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵) & ⊢ (𝜑 → 𝑋 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑋)) | ||
Theorem | fnlimfvre 41835* | 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 41836* | 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 41837* | The limit of complex number sequence 𝐹 is eventually approximated. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ (𝜑 → 𝐹 ⇝ 𝐴) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝑋 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋))) | ||
Theorem | fnlimfvre2 41838* | 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 41839* | The limit function of real functions, is a real-valued function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑚𝜑 & ⊢ Ⅎ𝑚𝐹 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚):dom (𝐹‘𝑚)⟶ℝ) & ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) ⇒ ⊢ (𝜑 → 𝐺:𝐷⟶ℝ) | ||
Theorem | fnlimabslt 41840* | 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 41841* | Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ Ⅎ𝑘𝐺 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → ( ⇝ ‘𝐹) = ( ⇝ ‘𝐺)) | ||
Theorem | climmptf 41842* | Exhibit a function 𝐺 with the same convergence properties as the not-quite-function 𝐹. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐺 = (𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴)) | ||
Theorem | climfveqmpt3 41843* | Two functions that are eventually equal to one another have the same limit. TODO: this is more general than climfveqmpt 41832 and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ (𝜑 → 𝑍 ⊆ 𝐴) & ⊢ (𝜑 → 𝑍 ⊆ 𝐶) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ 𝑈) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ( ⇝ ‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = ( ⇝ ‘(𝑘 ∈ 𝐶 ↦ 𝐷))) | ||
Theorem | climeldmeqf 41844* | 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 41845* | The limit of B convergent real sequence is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℝ) & ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ 𝐴) ⇝ 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ∈ ℝ) | ||
Theorem | limsupref 41846* | If a sequence is bounded, then the limsup is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝐹 & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (abs‘(𝐹‘𝑗)) ≤ 𝑏)) ⇒ ⊢ (𝜑 → (lim sup‘𝐹) ∈ ℝ) | ||
Theorem | limsupbnd1f 41847* | 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 41848* | A converging sequence of complex numbers is bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ∧ ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ∈ ℂ) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ≤ 𝑥) | ||
Theorem | climeqf 41849* | Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ Ⅎ𝑘𝐺 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴)) | ||
Theorem | climeldmeqmpt3 41850* | Two functions that are eventually equal, either both are convergent or both are divergent. TODO: this is more general than climeldmeqmpt 41829 and should replace it. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ (𝜑 → 𝑍 ⊆ 𝐴) & ⊢ (𝜑 → 𝑍 ⊆ 𝐶) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ 𝑈) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∈ dom ⇝ ↔ (𝑘 ∈ 𝐶 ↦ 𝐷) ∈ dom ⇝ )) | ||
Theorem | limsupcld 41851 | Closure of the superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) ⇒ ⊢ (𝜑 → (lim sup‘𝐹) ∈ ℝ*) | ||
Theorem | climfv 41852 | The limit of a convergent sequence, expressed as the function value of the convergence relation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐹 ⇝ 𝐴 → 𝐴 = ( ⇝ ‘𝐹)) | ||
Theorem | limsupval3 41853* | 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 41854* | Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑍 ⊆ 𝐴) & ⊢ (𝜑 → 𝑍 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → ( ⇝ ‘(𝑘 ∈ 𝐴 ↦ 𝐶)) = ( ⇝ ‘(𝑘 ∈ 𝐵 ↦ 𝐶))) | ||
Theorem | limsup0 41855 | The superior limit of the empty set (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (lim sup‘∅) = -∞ | ||
Theorem | climeldmeqmpt2 41856* | 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 41857 | 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 41858* | Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑍 ⊆ 𝐴) & ⊢ (𝜑 → 𝑍 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ⇝ 𝐷 ↔ (𝑥 ∈ 𝐵 ↦ 𝐶) ⇝ 𝐷)) | ||
Theorem | climfvd 41859 | The limit of a convergent sequence, expressed as the function value of the convergence relation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹 ⇝ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = ( ⇝ ‘𝐹)) | ||
Theorem | limsuplesup 41860 | An upper bound for the superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐾 ∈ ℝ) ⇒ ⊢ (𝜑 → (lim sup‘𝐹) ≤ sup(((𝐹 “ (𝐾[,)+∞)) ∩ ℝ*), ℝ*, < )) | ||
Theorem | limsupresico 41861 | 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 41862* | 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 41863* | 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 41864 | 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 41865* | If the limsup is not +∞, then the function is eventually bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝜑 & ⊢ Ⅎ𝑗𝐹 & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) & ⊢ (𝜑 → (lim sup‘𝐹) ≠ +∞) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) | ||
Theorem | limsupres 41866 | 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 41867* | A convergent, nonincreasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 𝑥 ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → 𝐹 ⇝ inf(ran 𝐹, ℝ*, < )) | ||
Theorem | climinf2 41868* | A convergent, nonincreasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 𝑥 ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → 𝐹 ⇝ inf(ran 𝐹, ℝ*, < )) | ||
Theorem | limsupvaluz 41869* | 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 41870 | 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 41871* | 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 41872* | 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 41873* | If the limsup is not +∞, then the function is bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝜑 & ⊢ Ⅎ𝑗𝑋 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝐾 ∈ ℝ) & ⊢ (𝜑 → ∀𝑗 ∈ 𝑍 (𝐾 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑌)) & ⊢ 𝑁 = if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾)) & ⊢ 𝑊 = sup(ran (𝑗 ∈ (𝑀...𝑁) ↦ (𝐹‘𝑗)), ℝ, < ) & ⊢ 𝑋 = if(𝑊 ≤ 𝑌, 𝑌, 𝑊) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑥) | ||
Theorem | limsupubuz 41874* | 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 41875* | 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 41876* | 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 41877* | A convergent, nonincreasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) & ⊢ (𝜑 → 𝐹 ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → 𝐹 ⇝ inf(ran 𝐹, ℝ*, < )) | ||
Theorem | limsupvaluzmpt 41878* | 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 41879* | 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 41880* | If the limsup is not +∞, then the function is eventually bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝜑 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (lim sup‘(𝑗 ∈ 𝑍 ↦ 𝐵)) ≠ +∞) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 𝐵 ≤ 𝑥) | ||
Theorem | limsupmnflem 41881* | 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 41882* | 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 41883* | 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 41884* | 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 41885* | 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 41886* | 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 41887* | 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 41888* | 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 | limsupequzmptlem 41889* | Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ 𝐴 = (ℤ≥‘𝑀) & ⊢ 𝐵 = (ℤ≥‘𝑁) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐵) → 𝐶 ∈ 𝑊) & ⊢ 𝐾 = if(𝑀 ≤ 𝑁, 𝑁, 𝑀) ⇒ ⊢ (𝜑 → (lim sup‘(𝑗 ∈ 𝐴 ↦ 𝐶)) = (lim sup‘(𝑗 ∈ 𝐵 ↦ 𝐶))) | ||
Theorem | limsupequzmpt 41890* | 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 | limsupre2mpt 41891* | 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 | limsupequzmptf 41892* | 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 | limsupre3lem 41893* | 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 less than or equal to the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝐹 & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) ⇒ ⊢ (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔ (∃𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)) ∧ ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)))) | ||
Theorem | limsupre3 41894* | 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 less than or equal to the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝐹 & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) ⇒ ⊢ (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔ (∃𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)) ∧ ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)))) | ||
Theorem | limsupre3mpt 41895* | 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 less than or equal to the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → ((lim sup‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ ↔ (∃𝑦 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑥 ∈ 𝐴 (𝑘 ≤ 𝑥 ∧ 𝑦 ≤ 𝐵) ∧ ∃𝑦 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑘 ≤ 𝑥 → 𝐵 ≤ 𝑦)))) | ||
Theorem | limsupre3uzlem 41896* | 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 less than or equal to the function, infinitely often; 2. there is a real number that is eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) ⇒ ⊢ (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔ (∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 ∃𝑗 ∈ (ℤ≥‘𝑘)𝑥 ≤ (𝐹‘𝑗) ∧ ∃𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥))) | ||
Theorem | limsupre3uz 41897* | 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 less than or equal to the function, infinitely often; 2. there is a real number that is eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) ⇒ ⊢ (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔ (∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 ∃𝑗 ∈ (ℤ≥‘𝑘)𝑥 ≤ (𝐹‘𝑗) ∧ ∃𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)(𝐹‘𝑗) ≤ 𝑥))) | ||
Theorem | limsupreuz 41898* | Given a function on the reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is less than or equal to the function, infinitely often; 2. there is a real number that is greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝐹 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ) ⇒ ⊢ (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔ (∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 ∃𝑗 ∈ (ℤ≥‘𝑘)𝑥 ≤ (𝐹‘𝑗) ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑥))) | ||
Theorem | limsupvaluz2 41899* | The superior limit, when the domain of a real-valued function is a set of upper integers, and the superior limit is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐹:𝑍⟶ℝ) & ⊢ (𝜑 → (lim sup‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → (lim sup‘𝐹) = inf(ran (𝑘 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ≥‘𝑘)), ℝ*, < )), ℝ, < )) | ||
Theorem | limsupreuzmpt 41900* | Given a function on the reals, defined on a set of upper integers, its supremum limit is real if and only if two condition holds: 1. there is a real number that is less than or equal to the function, infinitely often; 2. there is a real number that is greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((lim sup‘(𝑗 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ ↔ (∃𝑥 ∈ ℝ ∀𝑘 ∈ 𝑍 ∃𝑗 ∈ (ℤ≥‘𝑘)𝑥 ≤ 𝐵 ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 𝐵 ≤ 𝑥))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |