{ localUrl: '../page/real_number_as_cauchy_sequence.html', arbitalUrl: 'https://arbital.com/p/real_number_as_cauchy_sequence', rawJsonUrl: '../raw/50d.json', likeableId: '2912', likeableType: 'page', myLikeValue: '0', likeCount: '2', dislikeCount: '0', likeScore: '2', individualLikes: [ 'EricBruylant', 'JoeZeng' ], pageId: 'real_number_as_cauchy_sequence', edit: '9', editSummary: '', prevEdit: '8', currentEdit: '9', wasPublished: 'true', type: 'wiki', title: 'Real number (as Cauchy sequence)', clickbait: 'There are several ways to construct real numbers; this is the most natural way to use them in computations.', textLength: '2614', alias: 'real_number_as_cauchy_sequence', externalUrl: '', sortChildrenBy: 'likes', hasVote: 'false', voteType: '', votesAnonymous: 'false', editCreatorId: 'PatrickStevens', editCreatedAt: '2016-07-05 22:06:38', pageCreatorId: 'PatrickStevens', pageCreatedAt: '2016-07-02 14:09:15', seeDomainId: '0', editDomainId: 'AlexeiAndreev', submitToDomainId: '0', isAutosave: 'false', isSnapshot: 'false', isLiveEdit: 'true', isMinorEdit: 'false', indirectTeacher: 'false', todoCount: '0', isEditorComment: 'false', isApprovedComment: 'true', isResolved: 'false', snapshotText: '', anchorContext: '', anchorText: '', anchorOffset: '0', mergedInto: '', isDeleted: 'false', viewCount: '75', text: '[summary: If we want to construct the real numbers in terms of simpler objects (such as the rationals), one way to do it is to take our putative real number and consider sequences of rational numbers which in some sense "get closer and closer" to the real number.]\n\n[summary(Technical): The real numbers can be constructed as a field consisting of all Cauchy sequences of rationals, quotiented by the equivalence relation given by "two sequences are equivalent if and only if they eventually get arbitrarily close to each other".]\n\nConsider the set of all [53b Cauchy sequences] of [4zq rational numbers]: concretely, the set $$X = \\{ (a_n)_{n=1}^{\\infty} : a_n \\in \\mathbb{Q}, (\\forall \\epsilon \\in \\mathbb{Q}^{>0}) (\\exists N \\in \\mathbb{N})(\\forall n, m \\in \\mathbb{N}^{>N})(|a_n - a_m| < \\epsilon) \\}$$\n\nDefine an [-53y] on this set, by $(a_n) \\sim (b_n)$ if and only if, for every rational $\\epsilon > 0$, there is a [-45h] $N$ such that for all $n \\in \\mathbb{N}$ bigger than $N$, we have $|a_n - b_n| < \\epsilon$.\nThis is an equivalence relation (exercise).\n%%hidden(Show solution):\n- It is symmetric, because $|a_n - b_n| = |b_n - a_n|$.\n- It is reflexive, because $|a_n - a_n| = 0$ for every $n$, and this is $< \\epsilon$.\n- It is transitive, because if $|a_n - b_n| < \\frac{\\epsilon}{2}$ for sufficiently large $n$, and $|b_n - c_n| < \\frac{\\epsilon}{2}$ for sufficiently large $n$, then $|a_n - b_n| + |b_n - c_n| < \\frac{\\epsilon}{2} + \\frac{\\epsilon}{2} = \\epsilon$ for sufficiently large $n$; so by the [-triangle_inequality], $|a_n - c_n| < \\epsilon$ for sufficiently large $n$.\n%%\n\nWrite $[a_n]$ for the equivalence class of $(a_n)_{n=1}^{\\infty}$. (This is a slight abuse of notation, omitting the brackets that indicate that $a_n$ is actually a sequence rather than a rational number.)\n\nThe set of *real numbers* is the set of equivalence classes of $X$ under this equivalence relation, endowed with the following [540 totally ordered] [481 field] structure:\n\n- $[a_n] + [b_n] := [a_n + b_n]$\n- $[a_n] \\times [b_n] := [a_n \\times b_n]$\n- $[a_n] \\leq [b_n]$ if and only if $[a_n] = [b_n]$ or there is some $N$ such that for all $n > N$, $a_n \\leq b_n$.\n\nThis field structure is well-defined ([51h proof]).\n\n# Examples\n\n- Any rational number $r$ may be viewed as a real number, being the class $[r]$ (formally, the equivalence class of the sequence $(r, r, \\dots)$).\n- The real number $\\pi$ is indeed a real number under this definition; it is represented by, for instance, $(3, 3.1, 3.14, 3.141, \\dots)$. It is also represented as $(100, 3, 3.1, 3.14, \\dots)$, along with many other possibilities.', metaText: '', isTextLoaded: 'true', isSubscribedToDiscussion: 'false', isSubscribedToUser: 'false', isSubscribedAsMaintainer: 'false', discussionSubscriberCount: '1', maintainerCount: '1', userSubscriberCount: '0', lastVisit: '', hasDraft: 'false', votes: [], voteSummary: 'null', muVoteSummary: '0', voteScaling: '0', currentUserVote: '-2', voteCount: '0', lockedVoteType: '', maxEditEver: '0', redLinkCount: '0', lockedBy: '', lockedUntil: '', nextPageId: '', prevPageId: '', usedAsMastery: 'true', proposalEditNum: '0', permissions: { edit: { has: 'false', reason: 'You don't have domain permission to edit this page' }, proposeEdit: { has: 'true', reason: '' }, delete: { has: 'false', reason: 'You don't have domain permission to delete this page' }, comment: { has: 'false', reason: 'You can't comment in this domain because you are not a member' }, proposeComment: { has: 'true', reason: '' } }, summaries: {}, creatorIds: [ 'PatrickStevens', 'JoeZeng' ], childIds: [ 'reals_as_classes_of_cauchy_sequences_form_a_field' ], parentIds: [ 'real_number' ], commentIds: [ '50w' ], questionIds: [], tagIds: [], relatedIds: [], markIds: [], explanations: [], learnMore: [], requirements: [ { id: '4684', parentId: 'math3', childId: 'real_number_as_cauchy_sequence', type: 'requirement', creatorId: 'PatrickStevens', createdAt: '2016-07-02 14:10:44', level: '1', isStrong: 'false', everPublished: 'true' } ], subjects: [], lenses: [], lensParentId: 'real_number', pathPages: [], learnMoreTaughtMap: {}, learnMoreCoveredMap: {}, learnMoreRequiredMap: {}, editHistory: {}, domainSubmissions: {}, answers: [], answerCount: '0', commentCount: '0', newCommentCount: '0', linkedMarkCount: '0', changeLogs: [ { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '15472', pageId: 'real_number_as_cauchy_sequence', userId: 'PatrickStevens', edit: '9', type: 'newEdit', createdAt: '2016-07-05 22:06:38', auxPageId: '', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '15471', pageId: 'real_number_as_cauchy_sequence', userId: 'PatrickStevens', edit: '8', type: 'newEdit', createdAt: '2016-07-05 22:06:13', auxPageId: '', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '15406', pageId: 'real_number_as_cauchy_sequence', userId: 'PatrickStevens', edit: '7', type: 'newEdit', createdAt: '2016-07-05 19:11:59', auxPageId: '', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '2942', likeableType: 'changeLog', myLikeValue: '0', likeCount: '1', dislikeCount: '0', likeScore: '1', individualLikes: [], id: '15385', pageId: 'real_number_as_cauchy_sequence', userId: 'PatrickStevens', edit: '6', type: 'newEdit', createdAt: '2016-07-05 08:33:58', auxPageId: '', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '15287', pageId: 'real_number_as_cauchy_sequence', userId: 'EricBruylant', edit: '0', type: 'newChild', createdAt: '2016-07-04 19:08:29', auxPageId: 'reals_as_classes_of_cauchy_sequences_form_a_field', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '2931', likeableType: 'changeLog', myLikeValue: '0', likeCount: '1', dislikeCount: '0', likeScore: '1', individualLikes: [], id: '15240', pageId: 'real_number_as_cauchy_sequence', userId: 'PatrickStevens', edit: '5', type: 'newEdit', createdAt: '2016-07-04 12:55:30', auxPageId: '', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '15239', pageId: 'real_number_as_cauchy_sequence', userId: 'JoeZeng', edit: '4', type: 'newEdit', createdAt: '2016-07-04 12:51:21', auxPageId: '', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '15157', pageId: 'real_number_as_cauchy_sequence', userId: 'PatrickStevens', edit: '3', type: 'newEdit', createdAt: '2016-07-03 08:05:14', auxPageId: '', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '15118', pageId: 'real_number_as_cauchy_sequence', userId: 'PatrickStevens', edit: '2', type: 'newEdit', createdAt: '2016-07-02 14:15:04', auxPageId: '', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '15117', pageId: 'real_number_as_cauchy_sequence', userId: 'PatrickStevens', edit: '0', type: 'newRequirement', createdAt: '2016-07-02 14:10:45', auxPageId: 'math3', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '15113', pageId: 'real_number_as_cauchy_sequence', userId: 'PatrickStevens', edit: '0', type: 'newParent', createdAt: '2016-07-02 14:09:56', auxPageId: 'real_number', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '15111', pageId: 'real_number_as_cauchy_sequence', userId: 'PatrickStevens', edit: '1', type: 'newEdit', createdAt: '2016-07-02 14:09:15', auxPageId: '', oldSettingsValue: '', newSettingsValue: '' } ], feedSubmissions: [], searchStrings: {}, hasChildren: 'true', hasParents: 'true', redAliases: {}, improvementTagIds: [], nonMetaTagIds: [], todos: [], slowDownMap: 'null', speedUpMap: 'null', arcPageIds: 'null', contentRequests: {} }