![]() |
Metamath
Proof Explorer Theorem List (p. 342 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43661) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iblabsnc 34101* | Choice-free analogue of iblabs 24032. As with ibladdnc 34094, a measurability hypothesis is needed. (Contributed by Brendan Leahy, 7-Nov-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ 𝐿1) | ||
Theorem | iblmulc2nc 34102* | Choice-free analogue of iblmulc2 24034. (Contributed by Brendan Leahy, 17-Nov-2017.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿1) | ||
Theorem | itgmulc2nclem1 34103* | Lemma for itgmulc2nc 34105; cf. itgmulc2lem1 24035. (Contributed by Brendan Leahy, 17-Nov-2017.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥) | ||
Theorem | itgmulc2nclem2 34104* | Lemma for itgmulc2nc 34105; cf. itgmulc2lem2 24036. (Contributed by Brendan Leahy, 19-Nov-2017.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥) | ||
Theorem | itgmulc2nc 34105* | Choice-free analogue of itgmulc2 24037. (Contributed by Brendan Leahy, 19-Nov-2017.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥) | ||
Theorem | itgabsnc 34106* | Choice-free analogue of itgabs 24038. (Contributed by Brendan Leahy, 19-Nov-2017.) (Revised by Brendan Leahy, 19-Jun-2018.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn) & ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ ((∗‘∫𝐴𝐵 d𝑥) · ⦋𝑦 / 𝑥⦌𝐵)) ∈ MblFn) ⇒ ⊢ (𝜑 → (abs‘∫𝐴𝐵 d𝑥) ≤ ∫𝐴(abs‘𝐵) d𝑥) | ||
Theorem | bddiblnc 34107* | Choice-free proof of bddibl 24043. (Contributed by Brendan Leahy, 2-Nov-2017.) (Revised by Brendan Leahy, 6-Nov-2017.) |
⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 ∈ 𝐿1) | ||
Theorem | cnicciblnc 34108 | Choice-free proof of cniccibl 24044. (Contributed by Brendan Leahy, 2-Nov-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → 𝐹 ∈ 𝐿1) | ||
Theorem | itggt0cn 34109* | itggt0 24045 holds for continuous functions in the absence of ax-cc 9592. (Contributed by Brendan Leahy, 16-Nov-2017.) |
⊢ (𝜑 → 𝑋 < 𝑌) & ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐵) ∈ ((𝑋(,)𝑌)–cn→ℂ)) ⇒ ⊢ (𝜑 → 0 < ∫(𝑋(,)𝑌)𝐵 d𝑥) | ||
Theorem | ftc1cnnclem 34110* | Lemma for ftc1cnnc 34111; cf. ftc1lem4 24239. The stronger assumptions of ftc1cn 24243 are exploited to make use of weaker theorems. (Contributed by Brendan Leahy, 19-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝑐 ∈ (𝐴(,)𝐵)) & ⊢ 𝐻 = (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝑐}) ↦ (((𝐺‘𝑧) − (𝐺‘𝑐)) / (𝑧 − 𝑐))) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((abs‘(𝑦 − 𝑐)) < 𝑅 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝐸)) & ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → (abs‘(𝑋 − 𝑐)) < 𝑅) & ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → (abs‘(𝑌 − 𝑐)) < 𝑅) ⇒ ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝑋)) / (𝑌 − 𝑋)) − (𝐹‘𝑐))) < 𝐸) | ||
Theorem | ftc1cnnc 34111* | Choice-free proof of ftc1cn 24243. (Contributed by Brendan Leahy, 20-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) ⇒ ⊢ (𝜑 → (ℝ D 𝐺) = 𝐹) | ||
Theorem | ftc1anclem1 34112 | Lemma for ftc1anc 34120- the absolute value of a real-valued measurable function is measurable. Would be trivial with cncombf 23862, but this proof avoids ax-cc 9592. (Contributed by Brendan Leahy, 18-Jun-2018.) |
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐹 ∈ MblFn) → (abs ∘ 𝐹) ∈ MblFn) | ||
Theorem | ftc1anclem2 34113* | Lemma for ftc1anc 34120- restriction of an integrable function to the absolute value of its real or imaginary part. (Contributed by Brendan Leahy, 19-Jun-2018.) (Revised by Brendan Leahy, 8-Aug-2018.) |
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1 ∧ 𝐺 ∈ {ℜ, ℑ}) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) ∈ ℝ) | ||
Theorem | ftc1anclem3 34114 | Lemma for ftc1anc 34120- the absolute value of the sum of a simple function and i times another simple function is itself a simple function. (Contributed by Brendan Leahy, 27-May-2018.) |
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (abs ∘ (𝐹 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝐺))) ∈ dom ∫1) | ||
Theorem | ftc1anclem4 34115* | Lemma for ftc1anc 34120. (Contributed by Brendan Leahy, 17-Jun-2018.) |
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ 𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))))) ∈ ℝ) | ||
Theorem | ftc1anclem5 34116* | Lemma for ftc1anc 34120, the existence of a simple function the integral of whose pointwise difference from the function is less than a given positive real. (Contributed by Brendan Leahy, 17-Jun-2018.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) ⇒ ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌) | ||
Theorem | ftc1anclem6 34117* | Lemma for ftc1anc 34120- construction of simple functions within an arbitrary absolute distance of the given function. Similar to Lemma 565Ib of [Fremlin5] p. 218, but without Fremlin's additional step of converting the simple function into a continuous one, which is unnecessary to this lemma's use; also, two simple functions are used to allow for complex-valued 𝐹. (Contributed by Brendan Leahy, 31-May-2018.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) ⇒ ⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌) | ||
Theorem | ftc1anclem7 34118* | Lemma for ftc1anc 34120. (Contributed by Brendan Leahy, 13-May-2018.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) ⇒ ⊢ (((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) < ((𝑦 / 2) + (𝑦 / 2))) | ||
Theorem | ftc1anclem8 34119* | Lemma for ftc1anc 34120. (Contributed by Brendan Leahy, 29-May-2018.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) ⇒ ⊢ (((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) < 𝑦) | ||
Theorem | ftc1anc 34120* | ftc1a 24237 holds for functions that obey the triangle inequality in the absence of ax-cc 9592. Theorem 565Ma of [Fremlin5] p. 220. (Contributed by Brendan Leahy, 11-May-2018.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹 ∈ 𝐿1) & ⊢ (𝜑 → 𝐹:𝐷⟶ℂ) & ⊢ (𝜑 → ∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0)))) ⇒ ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) | ||
Theorem | ftc2nc 34121* | Choice-free proof of ftc2 24244. (Contributed by Brendan Leahy, 19-Jun-2018.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ)) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) ⇒ ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) | ||
Theorem | asindmre 34122 | Real part of domain of differentiability of arcsine. (Contributed by Brendan Leahy, 19-Dec-2018.) |
⊢ 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⇒ ⊢ (𝐷 ∩ ℝ) = (-1(,)1) | ||
Theorem | dvasin 34123* | Derivative of arcsine. (Contributed by Brendan Leahy, 18-Dec-2018.) |
⊢ 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⇒ ⊢ (ℂ D (arcsin ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 − (𝑥↑2))))) | ||
Theorem | dvacos 34124* | Derivative of arccosine. (Contributed by Brendan Leahy, 18-Dec-2018.) |
⊢ 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⇒ ⊢ (ℂ D (arccos ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (-1 / (√‘(1 − (𝑥↑2))))) | ||
Theorem | dvreasin 34125 | Real derivative of arcsine. (Contributed by Brendan Leahy, 3-Aug-2017.) (Proof shortened by Brendan Leahy, 18-Dec-2018.) |
⊢ (ℝ D (arcsin ↾ (-1(,)1))) = (𝑥 ∈ (-1(,)1) ↦ (1 / (√‘(1 − (𝑥↑2))))) | ||
Theorem | dvreacos 34126 | Real derivative of arccosine. (Contributed by Brendan Leahy, 3-Aug-2017.) (Proof shortened by Brendan Leahy, 18-Dec-2018.) |
⊢ (ℝ D (arccos ↾ (-1(,)1))) = (𝑥 ∈ (-1(,)1) ↦ (-1 / (√‘(1 − (𝑥↑2))))) | ||
Theorem | areacirclem1 34127* | Antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 28-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
⊢ (𝑅 ∈ ℝ+ → (ℝ D (𝑡 ∈ (-𝑅(,)𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))))) = (𝑡 ∈ (-𝑅(,)𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2)))))) | ||
Theorem | areacirclem2 34128* | Endpoint-inclusive continuity of Cartesian ordinate of circle. (Contributed by Brendan Leahy, 29-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) | ||
Theorem | areacirclem3 34129* | Integrability of cross-section of circle. (Contributed by Brendan Leahy, 26-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (2 · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ 𝐿1) | ||
Theorem | areacirclem4 34130* | Endpoint-inclusive continuity of antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
⊢ (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) | ||
Theorem | areacirclem5 34131* | Finding the cross-section of a circle. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} ⇒ ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅)) | ||
Theorem | areacirc 34132* | The area of a circle of radius 𝑅 is π · 𝑅↑2. This is Metamath 100 proof #9. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} ⇒ ⊢ ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (area‘𝑆) = (π · (𝑅↑2))) | ||
Theorem | anim12da 34133 | Conjoin antecedents and consequents in a deduction. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜃) & ⊢ ((𝜑 ∧ 𝜒) → 𝜏) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → (𝜃 ∧ 𝜏)) | ||
Theorem | unirep 34134* | Define a quantity whose definition involves a choice of representative, but which is uniquely determined regardless of the choice. (Contributed by Jeff Madsen, 1-Jun-2011.) |
⊢ (𝑦 = 𝐷 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐷 → 𝐵 = 𝐶) & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑧 → 𝐵 = 𝐹) & ⊢ 𝐵 ∈ V ⇒ ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → (℩𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) = 𝐶) | ||
Theorem | cover2 34135* | Two ways of expressing the statement "there is a cover of 𝐴 by elements of 𝐵 such that for each set in the cover, 𝜑". Note that 𝜑 and 𝑥 must be distinct. (Contributed by Jeff Madsen, 20-Jun-2010.) |
⊢ 𝐵 ∈ V & ⊢ 𝐴 = ∪ 𝐵 ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) ↔ ∃𝑧 ∈ 𝒫 𝐵(∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑)) | ||
Theorem | cover2g 34136* | Two ways of expressing the statement "there is a cover of 𝐴 by elements of 𝐵 such that for each set in the cover, 𝜑". Note that 𝜑 and 𝑥 must be distinct. (Contributed by Jeff Madsen, 21-Jun-2010.) |
⊢ 𝐴 = ∪ 𝐵 ⇒ ⊢ (𝐵 ∈ 𝐶 → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝜑) ↔ ∃𝑧 ∈ 𝒫 𝐵(∪ 𝑧 = 𝐴 ∧ ∀𝑦 ∈ 𝑧 𝜑))) | ||
Theorem | brabg2 34137* | Relation by a binary relation abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} & ⊢ (𝜒 → 𝐴 ∈ 𝐶) ⇒ ⊢ (𝐵 ∈ 𝐷 → (𝐴𝑅𝐵 ↔ 𝜒)) | ||
Theorem | opelopab3 34138* | Ordered pair membership in an ordered pair class abstraction, with a reduced hypothesis. (Contributed by Jeff Madsen, 29-May-2011.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝜒 → 𝐴 ∈ 𝐶) ⇒ ⊢ (𝐵 ∈ 𝐷 → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜒)) | ||
Theorem | cocanfo 34139 | Cancellation of a surjective function from the right side of a composition. (Contributed by Jeff Madsen, 1-Jun-2011.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺 Fn 𝐵 ∧ 𝐻 Fn 𝐵) ∧ (𝐺 ∘ 𝐹) = (𝐻 ∘ 𝐹)) → 𝐺 = 𝐻) | ||
Theorem | brresi2 34140 | Restriction of a binary relation. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴(𝑅 ↾ 𝐶)𝐵 → 𝐴𝑅𝐵) | ||
Theorem | fnopabeqd 34141* | Equality deduction for function abstractions. (Contributed by Jeff Madsen, 19-Jun-2011.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}) | ||
Theorem | fvopabf4g 34142* | Function value of an operator abstraction whose domain is a set of functions with given domain and range. (Contributed by Jeff Madsen, 1-Dec-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐶 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ (𝑅 ↑𝑚 𝐷) ↦ 𝐵) ⇒ ⊢ ((𝐷 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ∧ 𝐴:𝐷⟶𝑅) → (𝐹‘𝐴) = 𝐶) | ||
Theorem | eqfnun 34143 | Two functions on 𝐴 ∪ 𝐵 are equal if and only if they have equal restrictions to both 𝐴 and 𝐵. (Contributed by Jeff Madsen, 19-Jun-2011.) |
⊢ ((𝐹 Fn (𝐴 ∪ 𝐵) ∧ 𝐺 Fn (𝐴 ∪ 𝐵)) → (𝐹 = 𝐺 ↔ ((𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴) ∧ (𝐹 ↾ 𝐵) = (𝐺 ↾ 𝐵)))) | ||
Theorem | fnopabco 34144* | Composition of a function with a function abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 27-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶) & ⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} & ⊢ 𝐺 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐻‘𝐵))} ⇒ ⊢ (𝐻 Fn 𝐶 → 𝐺 = (𝐻 ∘ 𝐹)) | ||
Theorem | opropabco 34145* | Composition of an operator with a function abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) |
⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑅) & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝑆) & ⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 〈𝐵, 𝐶〉)} & ⊢ 𝐺 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐵𝑀𝐶))} ⇒ ⊢ (𝑀 Fn (𝑅 × 𝑆) → 𝐺 = (𝑀 ∘ 𝐹)) | ||
Theorem | f1opr 34146* | Condition for an operation to be one-to-one. (Contributed by Jeff Madsen, 17-Jun-2010.) |
⊢ (𝐹:(𝐴 × 𝐵)–1-1→𝐶 ↔ (𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ ∀𝑟 ∈ 𝐴 ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ∀𝑢 ∈ 𝐵 ((𝑟𝐹𝑠) = (𝑡𝐹𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))) | ||
Theorem | cocnv 34147 | Composition with a function and then with the converse. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((Fun 𝐹 ∧ Fun 𝐺) → ((𝐹 ∘ 𝐺) ∘ ◡𝐺) = (𝐹 ↾ ran 𝐺)) | ||
Theorem | f1ocan1fv 34148 | Cancel a composition by a bijection by preapplying the converse. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |
⊢ ((Fun 𝐹 ∧ 𝐺:𝐴–1-1-onto→𝐵 ∧ 𝑋 ∈ 𝐵) → ((𝐹 ∘ 𝐺)‘(◡𝐺‘𝑋)) = (𝐹‘𝑋)) | ||
Theorem | f1ocan2fv 34149 | Cancel a composition by the converse of a bijection by preapplying the bijection. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((Fun 𝐹 ∧ 𝐺:𝐴–1-1-onto→𝐵 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ ◡𝐺)‘(𝐺‘𝑋)) = (𝐹‘𝑋)) | ||
Theorem | inixp 34150* | Intersection of Cartesian products over the same base set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (X𝑥 ∈ 𝐴 𝐵 ∩ X𝑥 ∈ 𝐴 𝐶) = X𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) | ||
Theorem | upixp 34151* | Universal property of the indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝑋 = X𝑏 ∈ 𝐴 (𝐶‘𝑏) & ⊢ 𝑃 = (𝑤 ∈ 𝐴 ↦ (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑤))) ⇒ ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) → ∃!ℎ(ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) | ||
Theorem | abrexdom 34152* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑦 ∈ 𝐴 → ∃*𝑥𝜑) ⇒ ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝜑} ≼ 𝐴) | ||
Theorem | abrexdom2 34153* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = 𝐵} ≼ 𝐴) | ||
Theorem | ac6gf 34154* | Axiom of Choice. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | indexa 34155* | If for every element of an indexing set 𝐴 there exists a corresponding element of another set 𝐵, then there exists a subset of 𝐵 consisting only of those elements which are indexed by 𝐴. Used to avoid the Axiom of Choice in situations where only the range of the choice function is needed. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐵 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐(𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | indexdom 34156* | If for every element of an indexing set 𝐴 there exists a corresponding element of another set 𝐵, then there exists a subset of 𝐵 consisting only of those elements which are indexed by 𝐴, and which is dominated by the set 𝐴. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐴 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))) | ||
Theorem | frinfm 34157* | A subset of a well-founded set has an infimum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐶 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧))) | ||
Theorem | welb 34158* | A nonempty subset of a well-ordered set has a lower bound. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑅 We 𝐴 ∧ (𝐵 ∈ 𝐶 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → (◡𝑅 Or 𝐵 ∧ ∃𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧)))) | ||
Theorem | supex2g 34159 | Existence of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 ∈ 𝐶 → sup(𝐵, 𝐴, 𝑅) ∈ V) | ||
Theorem | supclt 34160* | Closure of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑅 Or 𝐴 ∧ ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) → sup(𝐵, 𝐴, 𝑅) ∈ 𝐴) | ||
Theorem | supubt 34161* | Upper bound property of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑅 Or 𝐴 ∧ ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) → (𝐶 ∈ 𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶)) | ||
Theorem | filbcmb 34162* | Combine a finite set of lower bounds. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑦 ≤ 𝑧 → 𝜑) → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑦 ≤ 𝑧 → ∀𝑥 ∈ 𝐴 𝜑))) | ||
Theorem | fzmul 34163 | Membership of a product in a finite interval of integers. (Contributed by Jeff Madsen, 17-Jun-2010.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ) → (𝐽 ∈ (𝑀...𝑁) → (𝐾 · 𝐽) ∈ ((𝐾 · 𝑀)...(𝐾 · 𝑁)))) | ||
Theorem | sdclem2 34164* | Lemma for sdc 34166. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓 ↔ 𝜒)) & ⊢ (𝑛 = 𝑀 → (𝜓 ↔ 𝜏)) & ⊢ (𝑛 = 𝑘 → (𝜓 ↔ 𝜃)) & ⊢ ((𝑔 = ℎ ∧ 𝑛 = (𝑘 + 1)) → (𝜓 ↔ 𝜎)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → ∃𝑔(𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃) → ∃ℎ(ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎))) & ⊢ 𝐽 = {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} & ⊢ 𝐹 = (𝑤 ∈ 𝑍, 𝑥 ∈ 𝐽 ↦ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) & ⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐺:𝑍⟶𝐽) & ⊢ (𝜑 → (𝐺‘𝑀):(𝑀...𝑀)⟶𝐴) & ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝐺‘(𝑤 + 1)) ∈ (𝑤𝐹(𝐺‘𝑤))) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒)) | ||
Theorem | sdclem1 34165* | Lemma for sdc 34166. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓 ↔ 𝜒)) & ⊢ (𝑛 = 𝑀 → (𝜓 ↔ 𝜏)) & ⊢ (𝑛 = 𝑘 → (𝜓 ↔ 𝜃)) & ⊢ ((𝑔 = ℎ ∧ 𝑛 = (𝑘 + 1)) → (𝜓 ↔ 𝜎)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → ∃𝑔(𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃) → ∃ℎ(ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎))) & ⊢ 𝐽 = {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} & ⊢ 𝐹 = (𝑤 ∈ 𝑍, 𝑥 ∈ 𝐽 ↦ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒)) | ||
Theorem | sdc 34166* | Strong dependent choice. Suppose we may choose an element of 𝐴 such that property 𝜓 holds, and suppose that if we have already chosen the first 𝑘 elements (represented here by a function from 1...𝑘 to 𝐴), we may choose another element so that all 𝑘 + 1 elements taken together have property 𝜓. Then there exists an infinite sequence of elements of 𝐴 such that the first 𝑛 terms of this sequence satisfy 𝜓 for all 𝑛. This theorem allows us to construct infinite seqeunces where each term depends on all the previous terms in the sequence. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 3-Jun-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓 ↔ 𝜒)) & ⊢ (𝑛 = 𝑀 → (𝜓 ↔ 𝜏)) & ⊢ (𝑛 = 𝑘 → (𝜓 ↔ 𝜃)) & ⊢ ((𝑔 = ℎ ∧ 𝑛 = (𝑘 + 1)) → (𝜓 ↔ 𝜎)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → ∃𝑔(𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃) → ∃ℎ(ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎))) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒)) | ||
Theorem | fdc 34167* | Finite version of dependent choice. Construct a function whose value depends on the previous function value, except at a final point at which no new value can be chosen. The final hypothesis ensures that the process will terminate. The proof does not use the Axiom of Choice. (Contributed by Jeff Madsen, 18-Jun-2010.) |
⊢ 𝐴 ∈ V & ⊢ 𝑀 ∈ ℤ & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑁 = (𝑀 + 1) & ⊢ (𝑎 = (𝑓‘(𝑘 − 1)) → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = (𝑓‘𝑘) → (𝜓 ↔ 𝜒)) & ⊢ (𝑎 = (𝑓‘𝑛) → (𝜃 ↔ 𝜏)) & ⊢ (𝜂 → 𝐶 ∈ 𝐴) & ⊢ (𝜂 → 𝑅 Fr 𝐴) & ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (𝜃 ∨ ∃𝑏 ∈ 𝐴 𝜑)) & ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏𝑅𝑎) ⇒ ⊢ (𝜂 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) | ||
Theorem | fdc1 34168* | Variant of fdc 34167 with no specified base value. (Contributed by Jeff Madsen, 18-Jun-2010.) |
⊢ 𝐴 ∈ V & ⊢ 𝑀 ∈ ℤ & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑁 = (𝑀 + 1) & ⊢ (𝑎 = (𝑓‘𝑀) → (𝜁 ↔ 𝜎)) & ⊢ (𝑎 = (𝑓‘(𝑘 − 1)) → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = (𝑓‘𝑘) → (𝜓 ↔ 𝜒)) & ⊢ (𝑎 = (𝑓‘𝑛) → (𝜃 ↔ 𝜏)) & ⊢ (𝜂 → ∃𝑎 ∈ 𝐴 𝜁) & ⊢ (𝜂 → 𝑅 Fr 𝐴) & ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (𝜃 ∨ ∃𝑏 ∈ 𝐴 𝜑)) & ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏𝑅𝑎) ⇒ ⊢ (𝜂 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ (𝜎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) | ||
Theorem | seqpo 34169* | Two ways to say that a sequence respects a partial order. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) → (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ↔ ∀𝑚 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘(𝑚 + 1))(𝐹‘𝑚)𝑅(𝐹‘𝑛))) | ||
Theorem | incsequz 34170* | An increasing sequence of positive integers takes on indefinitely large values. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)) ∧ 𝐴 ∈ ℕ) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ≥‘𝐴)) | ||
Theorem | incsequz2 34171* | An increasing sequence of positive integers takes on indefinitely large values. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)) ∧ 𝐴 ∈ ℕ) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ (ℤ≥‘𝐴)) | ||
Theorem | nnubfi 34172* | A bounded above set of positive integers is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Feb-2014.) |
⊢ ((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) → {𝑥 ∈ 𝐴 ∣ 𝑥 < 𝐵} ∈ Fin) | ||
Theorem | nninfnub 34173* | An infinite set of positive integers is unbounded above. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Feb-2014.) |
⊢ ((𝐴 ⊆ ℕ ∧ ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ ℕ) → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} ≠ ∅) | ||
Theorem | subspopn 34174 | An open set is open in the subspace topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝐽 ∧ 𝐵 ⊆ 𝐴)) → 𝐵 ∈ (𝐽 ↾t 𝐴)) | ||
Theorem | neificl 34175 | Neighborhoods are closed under finite intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 25-Nov-2013.) |
⊢ (((𝐽 ∈ Top ∧ 𝑁 ⊆ ((nei‘𝐽)‘𝑆)) ∧ (𝑁 ∈ Fin ∧ 𝑁 ≠ ∅)) → ∩ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) | ||
Theorem | lpss2 34176 | Limit points of a subset are limit points of the larger set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((limPt‘𝐽)‘𝐵) ⊆ ((limPt‘𝐽)‘𝐴)) | ||
Theorem | metf1o 34177* | Use a bijection with a metric space to construct a metric on a set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝑁 = (𝑥 ∈ 𝑌, 𝑦 ∈ 𝑌 ↦ ((𝐹‘𝑥)𝑀(𝐹‘𝑦))) ⇒ ⊢ ((𝑌 ∈ 𝐴 ∧ 𝑀 ∈ (Met‘𝑋) ∧ 𝐹:𝑌–1-1-onto→𝑋) → 𝑁 ∈ (Met‘𝑌)) | ||
Theorem | blssp 34178 | A ball in the subspace metric. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jan-2014.) |
⊢ 𝑁 = (𝑀 ↾ (𝑆 × 𝑆)) ⇒ ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑌 ∈ 𝑆 ∧ 𝑅 ∈ ℝ+)) → (𝑌(ball‘𝑁)𝑅) = ((𝑌(ball‘𝑀)𝑅) ∩ 𝑆)) | ||
Theorem | mettrifi 34179* | Generalized triangle inequality for arbitrary finite sums. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 4-Jun-2014.) |
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝑋) ⇒ ⊢ (𝜑 → ((𝐹‘𝑀)𝐷(𝐹‘𝑁)) ≤ Σ𝑘 ∈ (𝑀...(𝑁 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) | ||
Theorem | lmclim2 34180* | A sequence in a metric space converges to a point iff the distance between the point and the elements of the sequence converges to 0. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) |
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑋) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐺 = (𝑥 ∈ ℕ ↦ ((𝐹‘𝑥)𝐷𝑌)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑌 ↔ 𝐺 ⇝ 0)) | ||
Theorem | geomcau 34181* | If the distance between consecutive points in a sequence is bounded by a geometric sequence, then the sequence is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) |
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑋) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 < 1) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (𝐵↑𝑘))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷)) | ||
Theorem | caures 34182 | The restriction of a Cauchy sequence to an upper set of integers is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jun-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (𝑋 ↑pm ℂ)) ⇒ ⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ↾ 𝑍) ∈ (Cau‘𝐷))) | ||
Theorem | caushft 34183* | A shifted Cauchy sequence is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jun-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ 𝑊 = (ℤ≥‘(𝑀 + 𝑁)) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐺‘(𝑘 + 𝑁))) & ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷)) & ⊢ (𝜑 → 𝐺:𝑊⟶𝑋) ⇒ ⊢ (𝜑 → 𝐺 ∈ (Cau‘𝐷)) | ||
Theorem | constcncf 34184* | A constant function is a continuous function on ℂ. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved into main set.mm as cncfmptc 23122 and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ 𝐴) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | idcncf 34185 | The identity function is a continuous function on ℂ. (Contributed by Jeff Madsen, 11-Jun-2010.) (Moved into main set.mm as cncfmptid 23123 and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ 𝑥) ⇒ ⊢ 𝐹 ∈ (ℂ–cn→ℂ) | ||
Theorem | sub1cncf 34186* | Subtracting a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 − 𝐴)) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | sub2cncf 34187* | Subtraction from a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 − 𝑥)) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | cnres2 34188* | The restriction of a continuous function to a subset is continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐹 ∈ (𝐽 Cn 𝐾) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn (𝐾 ↾t 𝐵))) | ||
Theorem | cnresima 34189 | A continuous function is continuous onto its image. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (𝐽 Cn (𝐾 ↾t ran 𝐹))) | ||
Theorem | cncfres 34190* | A continuous function on complex numbers restricted to a subset. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐴 ⊆ ℂ & ⊢ 𝐵 ⊆ ℂ & ⊢ 𝐹 = (𝑥 ∈ ℂ ↦ 𝐶) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵) & ⊢ 𝐹 ∈ (ℂ–cn→ℂ) & ⊢ 𝐽 = (MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))) & ⊢ 𝐾 = (MetOpen‘((abs ∘ − ) ↾ (𝐵 × 𝐵))) ⇒ ⊢ 𝐺 ∈ (𝐽 Cn 𝐾) | ||
Syntax | ctotbnd 34191 | Extend class notation with the class of totally bounded metric spaces. |
class TotBnd | ||
Syntax | cbnd 34192 | Extend class notation with the class of bounded metric spaces. |
class Bnd | ||
Definition | df-totbnd 34193* | Define the class of totally bounded metrics. A metric space is totally bounded iff it can be covered by a finite number of balls of any given radius. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ TotBnd = (𝑥 ∈ V ↦ {𝑚 ∈ (Met‘𝑥) ∣ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑥 ∧ ∀𝑏 ∈ 𝑣 ∃𝑦 ∈ 𝑥 𝑏 = (𝑦(ball‘𝑚)𝑑))}) | ||
Theorem | istotbnd 34194* | The predicate "is a totally bounded metric space". (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑋 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) | ||
Theorem | istotbnd2 34195* | The predicate "is a totally bounded metric space." (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑀 ∈ (Met‘𝑋) → (𝑀 ∈ (TotBnd‘𝑋) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (∪ 𝑣 = 𝑋 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) | ||
Theorem | istotbnd3 34196* | A metric space is totally bounded iff there is a finite ε-net for every positive ε. This differs from the definition in providing a finite set of ball centers rather than a finite set of balls. (Contributed by Mario Carneiro, 12-Sep-2015.) |
⊢ (𝑀 ∈ (TotBnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑) = 𝑋)) | ||
Theorem | totbndmet 34197 | The predicate "totally bounded" implies 𝑀 is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑀 ∈ (TotBnd‘𝑋) → 𝑀 ∈ (Met‘𝑋)) | ||
Theorem | 0totbnd 34198 | The metric (there is only one) on the empty set is totally bounded. (Contributed by Mario Carneiro, 16-Sep-2015.) |
⊢ (𝑋 = ∅ → (𝑀 ∈ (TotBnd‘𝑋) ↔ 𝑀 ∈ (Met‘𝑋))) | ||
Theorem | sstotbnd2 34199* | Condition for a subset of a metric space to be totally bounded. (Contributed by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ (𝒫 𝑋 ∩ Fin)𝑌 ⊆ ∪ 𝑥 ∈ 𝑣 (𝑥(ball‘𝑀)𝑑))) | ||
Theorem | sstotbnd 34200* | Condition for a subset of a metric space to be totally bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝑁 = (𝑀 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑁 ∈ (TotBnd‘𝑌) ↔ ∀𝑑 ∈ ℝ+ ∃𝑣 ∈ Fin (𝑌 ⊆ ∪ 𝑣 ∧ ∀𝑏 ∈ 𝑣 ∃𝑥 ∈ 𝑋 𝑏 = (𝑥(ball‘𝑀)𝑑)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |