25:["$","title",null,{"children":"MetSp 2022 chapter 02: The real line | kkytola | Observable"}] 4b:T49c,myFormulas = String.raw`import topology.algebra.module /-- **Lemma**: The composition g ∘ f : X → Z of two continuous functions f : X → Y and g : Y → Z is continuous. -/ lemma testing {X Y Z : Type} [topological_space X] [topological_space Y] [topological_space Z] (f : X → Y) (f_cont : continuous f) (g : Y → Z) (g_cont : continuous g) : continuous (g ∘ f) := begin -- Unfold the definition of continuity at the goal and hypotheses: a function is continuous -- if the preimage of every open subset of the codomain is open. rw continuous_def at *, -- Let U ⊆ Z be an open subset in the space Z. intro U, assume U_open, -- By continuity of g, we have that the preimage g⁻¹ U ⊆ Y is an open subset in the space Y. have g_pre_U_open : is_open (g ⁻¹' U), from g_cont _ U_open, -- By continuity of f, we then have that the preimage f⁻¹ (g⁻¹ U) ⊆ X is an open subset -- in the space X. have f_pre_g_pre_U_open : is_open (f ⁻¹' (g ⁻¹' U)), from f_cont _ g_pre_U_open, -- Since f⁻¹ (g⁻¹ U) = (g ∘ f)⁻¹ U, this is exactly what we wanted to show. exact f_pre_g_pre_U_open, end`.split('\n---\n')4c:[{"id":"63b632600b671be558ef8f67e7bc0d62d7d81877ff766ebb67270c6e59699a34e820fa9afb8d5baf5b254bc0fe874eebb3b85723628afb561d14cb24b3d9172d","href":"https://static.observableusercontent.com/files/63b632600b671be558ef8f67e7bc0d62d7d81877ff766ebb67270c6e59699a34e820fa9afb8d5baf5b254bc0fe874eebb3b85723628afb561d14cb24b3d9172d","name":"metsp_obs_lean_02@3.lean","type":"application/octet-stream","lastModified":1642084939311.186,"size":37052},{"id":"311f782623b09f539c59617524d38f8ce1cbbbf8f14a715931f5f26d8b3513ec051d40a1b766f09cf1bdfdfb22873700c24fc89a8525c980219672ba510d1203","href":"https://static.observableusercontent.com/files/311f782623b09f539c59617524d38f8ce1cbbbf8f14a715931f5f26d8b3513ec051d40a1b766f09cf1bdfdfb22873700c24fc89a8525c980219672ba510d1203","name":"sequencelimit-01.png","type":"image/png","lastModified":1640915453518.131,"size":7635},{"id":"55d26e6018f9b747bfd27a3de7fe4731f02cc47c3812119b8ad5f4371a9311281a6f8553c67a1a85b8cd6b2a2e90adfd5c865f9c279092f099cc7913d2a3f9d1","href":"https://static.observableusercontent.com/files/55d26e6018f9b747bfd27a3de7fe4731f02cc47c3812119b8ad5f4371a9311281a6f8553c67a1a85b8cd6b2a2e90adfd5c865f9c279092f099cc7913d2a3f9d1","name":"real_line-1.png","type":"image/png","lastModified":1641925016557.693,"size":3263},{"id":"72cf65d3803ee7e55d10e3a996e00cbf7427d7d233d70c3ca8acac31b6d17a0b743f4edafbac77f7e819253cd6fd47da8bf73eb91ca3d9b9421228631e573ea4","href":"https://static.observableusercontent.com/files/72cf65d3803ee7e55d10e3a996e00cbf7427d7d233d70c3ca8acac31b6d17a0b743f4edafbac77f7e819253cd6fd47da8bf73eb91ca3d9b9421228631e573ea4","name":"metsp_obs_lean_02@1.lean","type":"application/octet-stream","lastModified":1641937788323.512,"size":34648},{"id":"d6ae5b7be1e37768d4bcec776bbcf5829b7e8b79d0342c41808d2ee053ee8f2cfea260ccab5469c6672569ff44be475aea90fac475e7fba000d3dd6e58513d6e","href":"https://static.observableusercontent.com/files/d6ae5b7be1e37768d4bcec776bbcf5829b7e8b79d0342c41808d2ee053ee8f2cfea260ccab5469c6672569ff44be475aea90fac475e7fba000d3dd6e58513d6e","name":"metsp_obs_lean_02@2.lean","type":"application/octet-stream","lastModified":1642084288642.097,"size":36955}] 47:{"id":"ead7e9bb33a60312","slug":"metsp2022_lec02","title":"MetSp 2022 chapter 02: The real line","thumbnail":"e21973ae45d9aa9e2d89eab514a7cc7e50c37bf09e2013c074897830b1977335","access_level":"unlisted","create_time":"$D2021-12-30T23:34:31.144Z","update_time":"$D2022-01-13T14:42:31.537Z","view_time":null,"first_public_time":null,"has_unpublished_edits":null,"fork":true,"stars":0,"starred":false,"owner":{"type":"team","id":"b8c04148a2c6e789","login":"kkytola","name":"","avatar_url":"https://avatars-next.observableusercontent.com/3ae82de79f44c0c40dcdaca986538cd3c5637da2ca75e0d6b7af3f2cfc754305","tier":"starter_2024","bio":"","followed_by_you":false,"follows_you":false},"version":574,"publish_version":574,"role":null,"authored":false,"authors":[{"type":"individual","id":"1c4c50ca040e47ea","login":"kkytola","name":"","avatar_url":"https://avatars-next.observableusercontent.com/3ae82de79f44c0c40dcdaca986538cd3c5637da2ca75e0d6b7af3f2cfc754305","tier":null,"bio":"","followed_by_you":false,"follows_you":false}],"members":[{"type":"individual","id":"1c4c50ca040e47ea","login":"kkytola","name":"","avatar_url":"https://avatars-next.observableusercontent.com/3ae82de79f44c0c40dcdaca986538cd3c5637da2ca75e0d6b7af3f2cfc754305","tier":null,"role":"editor"}],"comments":[],"custom_thumbnail":false,"trashed":false,"lapsed":null,"subscribed":null,"forks":0,"collection":null,"type":"notebook","body":{"titling":"auto","title":"MetSp 2022 chapter 02: The real line","cells":[{"id":0,"value":"# MetSp 2022 chapter 02: The real line","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":113,"value":"*This notebook is meant as supporting material for parts of Chapter II of my lecture notes*\n\n>> *[Metric Spaces](https://github.com/kkytola/Metric-spaces-materials/blob/main/MetSp-2022.pdf). (Download the pdf-file from GitHub to see the full file.)*\n\n*In particular, the numbering of Definitions, Theorems, Examples, etc., refers to these lecture notes.*","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":117,"value":"*This notebook uses [Lean](https://leanprover-community.github.io/) to explore some proofs with the help of the computer. The Observable notebook implementation of Lean is from [@bryangingechen](https://observablehq.com/@bryangingechen)'s [Lean collection](https://observablehq.com/collection/@bryangingechen/lean). Note that the cache required for running the Lean code here is close to 60MB, so it will probably not work on mobile devices and it might require a few minutes to start on a computer.*","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":42,"value":"### Overview","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":178,"value":"FileAttachment(\"real_line-1.png\").image()","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":47,"value":"##### Key definitions:\n\n * ...","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":54,"value":"##### Key results:\n\n * ...","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":93,"value":"##### Key examples:\n\n * ...","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":60,"value":"##### Key ideas:\n\n * ...","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":64,"value":"## Today's math","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":540,"value":"A real-number sequence is a function ${tex`a \\colon \\N \\to \\R`}. \nIt can be viewed as an infinite list of the form ${tex`(a_1 , a_2 , a_3 , \\ldots)`}, with ${tex`a_n = a(n)`} for ${tex`n \\in \\N`}.","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":133,"value":"### Limits of sequences of real numbers","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":110,"value":"FileAttachment(\"sequencelimit-01.png\").image()","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":165,"value":"**Definition II.11** (Limit of a sequence of numbers)\n> A sequence ${tex`(a_n)_{n \\in \\mathbb{N}}`} of real numbers **converges** to a **limit** ${tex`\\alpha \\in \\mathbb{R}`} if for every ${tex`{\\varepsilon> 0}`} there exists an index ${tex`{n_\\varepsilon\\in \\mathbb{N}}`} such that ${tex`{|a_n - \\alpha| < \\varepsilon}`} whenever ${tex`{n \\geq n_\\varepsilon}`}. ","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":169,"value":"If a sequence ${tex`(a_n)_{n \\in \\mathbb{N}}`} converges to a limit ${tex`\\alpha`} in the sense of the above definition, we denote ${tex.block`\\begin{aligned} \\lim_{n \\to \\infty} a_n = \\alpha .\\end{aligned}`} Alternatively, it is common to say that ${tex`a_n \\to \\alpha`} as ${tex`n \\to \\infty`}, or that the sequence ${tex`(a_n)_{n \\in \\mathbb{N}}`} tends to ${tex`\\alpha`} (as ${tex`n \\to \\infty`}). ","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":419,"value":"viewof limit_lean = nbFormulasEditor(limit_label, invalidation, { height: 60, header: html``})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":185,"value":" **Lemma II.14** (Preservation of inequalities)\n > Let ${tex`(a_n)_{n \\in \\mathbb{N}}`} and ${tex`(b_n)_{n \\in \\mathbb{N}}`} be two convergent sequences of real numbers, with respective limits ${tex`\\alpha = \\lim_{n \\to \\infty} a_n`} and ${tex`\\beta = \\lim_{n \\to \\infty} b_n`}. If we have ${tex.block`\\begin{aligned} a_n \\leq b_n \\qquad \\text{ for all $n \\in \\mathbb{N}$, }\\end{aligned}`} then we also have the corresponding inequality ${tex.block`\\begin{aligned} \\alpha \\; = \\; \\lim_{n \\to \\infty} a_n \\; \\leq \\; \\lim_{n \\to \\infty} b_n \\; = \\; \\beta\\end{aligned}`} for the limits. \n","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":258,"value":"viewof preservation_ineq_lean = nbFormulasEditor(preservation_ineq_label, invalidation, { height: 60, header: html``})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":181,"value":" **Corollary II.16** (Uniqueness of limits of real-number sequences)\"\n > Let ${tex`(a_n)_{n \\in \\mathbb{N}}`} be a sequence of real numbers. If both ${tex`\\alpha \\in \\mathbb{R}`} and ${tex`\\alpha' \\in \\mathbb{R}`} are limits of this sequence, then ${tex`\\alpha = \\alpha'`}. ","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":413,"value":"viewof uniqueness_of_lim_lean = nbFormulasEditor(uniqueness_of_lim_label, invalidation, { height: 60, header: html``})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":140,"value":"## Monotonicity","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":145,"value":" **Definition II.4** (Monotonicity properties of sequences of real numbers)\n > A real-number sequence ${tex`(a_n)_{n \\in \\mathbb{N}}`} is \n - **increasing**, if we have ${tex`a_{n+1} \\geq a_n`} for all ${tex`n \\in \\mathbb{N}`} \n - **strictly increasing**, if we have ${tex`a_{n+1} > a_n`} for all ${tex`n \\in \\mathbb{N}`} \n - **decreasing**, if we have ${tex`a_{n+1} \\leq a_n`} for all ${tex`n \\in \\mathbb{N}`} \n - **strictly decreasing**, if we have ${tex`a_{n+1} < a_n`} for all ${tex`n \\in \\mathbb{N}`} \n - **monotone**, if it is either increasing or decreasing. \n","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":154,"value":"### Boundedness","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":150,"value":"**Definition II.8** (Boundedness properties of sequences of real numbers)\n> A real-number sequence ${tex`(a_n)_{n \\in \\mathbb{N}}`} is \n - **bounded from above**, if there exists some ${tex`u\\in \\mathbb{R}`} (called an **upper bound** for the sequence) such that ${tex`a_{n} \\leq u`} for all ${tex`n \\in \\mathbb{N}`}; \n - **bounded from below**, if there exists some ${tex`\\ell\\in \\mathbb{R}`} (called a **lower bound** for the sequence) such that ${tex`a_{n} \\geq \\ell`} for all ${tex`n \\in \\mathbb{N}`}; \n - **bounded**, if there exists some ${tex`r\\in \\mathbb{R}`} such that ${tex`|a_{n}| \\leq r`} for all ${tex`n \\in \\mathbb{N}`}. ","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":422,"value":"viewof seq_upper_bound_lean = nbFormulasEditor(seq_upper_bound_label, invalidation, { height: 60, header: html``})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":426,"value":"viewof seq_upper_bounded_lean = nbFormulasEditor(seq_upper_bounded_label, invalidation, { height: 60, header: html``})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":430,"value":"viewof seq_bound_lean = nbFormulasEditor(seq_bound_label, invalidation, { height: 60, header: html``})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":436,"value":"viewof seq_bounded_lean = nbFormulasEditor(seq_bounded_label, invalidation, { height: 60, header: html``})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":156,"value":"**Exercise II.2** (Boundedness from both above and below).\n > Prove that a real-number sequence ${tex`(a_n)_{n \\in \\mathbb{N}}`} is bounded if and only if it is both bounded from above and bounded from below. \n","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":439,"value":"viewof seq_bounded_iff_lean = nbFormulasEditor(seq_bounded_iff_both_label, invalidation, { height: 60, header: html``})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":553,"value":"**Theorem II.13** (A convergent sequence of number is bounded)\n> If a sequence ${tex`(a_n)_{n \\in \\mathbb{N}}`} of real numbers converges, then it is bounded. \n","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":559,"value":"viewof conv_imp_bdd_lean = nbFormulasEditor(conv_imp_bdd_label, invalidation, { height: 60, header: html``})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":564,"value":"**Exercise II.5** (Boundedness does not imply convergence).\n> Show that there exists a bounded sequence which is not convergent. Conclude that the implication in the converse direction compared to Theorem II.13 does not hold.","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":189,"value":"**Theorem II.19** (Rules of calculation with limits)\n> Let ${tex`(a_n)_{n \\in \\mathbb{N}}`} and ${tex`(b_n)_{n \\in \\mathbb{N}}`} be two convergent sequences with respective limits ${tex`{\\alpha = \\lim_{n \\to \\infty} a_n}`} and ${tex`{\\beta = \\lim_{n \\to \\infty} b_n}`}. Then we have ${tex.block`\\begin{aligned} \\lim_{n \\to \\infty} (a_n + b_n) \\; = \\;\\;& \\alpha + \\beta , \\\\ \n\\lim_{n \\to \\infty} (a_n \\, b_n) \\; = \\;\\;& \\alpha \\beta ,\\end{aligned}`} and if moreover ${tex`\\beta \\neq 0`}, then ${tex.block`\\begin{aligned} \\lim_{n \\to \\infty} \\frac{a_n}{b_n} \\; = \\;\\;& \\frac{\\alpha}{\\beta} .\\end{aligned}`} \n","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":196,"value":"### Axioms of real numbers","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":200,"value":"The set of real numbers is denoted by ${tex`\\mathbb{R}`}, and it is equipped with two binary operations:\n * addition, ${tex`\\mathbb{R}\\times \\mathbb{R}\\to \\mathbb{R}`}, ${tex`(x,y) \\mapsto x+y`}\n * multiplication, ${tex`\\mathbb{R}\\times \\mathbb{R}\\to \\mathbb{R}`}, ${tex`(x,y) \\mapsto x \\cdot y`}\n\nand a binary relation\n * less than, ${tex`<`}.\n\nThe axioms of real numbers fall into three types: the *field axioms* concern only the operations of addition and multiplication, the *order axioms* concern the order relation ${tex`<`} and how it behaves under addition and multiplication, and finally the *completeness axiom* which is in many ways the most subtle. \n","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":207,"value":"### Completeness axiom","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":213,"value":"**Definition II.25** (Upper and lower bounds)\n> Let ${tex`A \\subset \\mathbb{R}`} be a subset. \n\n> A real number ${tex`u\\in \\mathbb{R}`} is an **upper bound** for ${tex`A`} if for all ${tex`a \\in A`} we have ${tex`a \\leq u`}. \n\n> A real number ${tex`\\ell\\in \\mathbb{R}`} is a **lower bound** for ${tex`A`} if for all ${tex`a \\in A`} we have ${tex`a \\geq \\ell`}. \n","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":536,"value":"**Examples:**\n * The set ${tex`A = \\{ n \\in \\Z \\; | \\; n < 0\\}`} (the negative integers) has ${tex`+361`} as an upper bound.\n * The set ${tex`\\R \\subset \\R`} does not have any upper bound.","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":547,"value":"viewof set_upbd_lean = nbFormulasEditor(set_upbd_label, invalidation, { height: 60, header: html``})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":550,"value":"viewof set_lowbd_lean = nbFormulasEditor(set_lowbd_label, invalidation, { height: 60, header: html``})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":217,"value":" **Definition II.28** (Supremum and infimum)\n \n> Let ${tex`A \\subset \\mathbb{R}`} be a nonempty subset (${tex`A \\neq \\emptyset`}) which is bounded from above. A number ${tex`u_0 \\in \\mathbb{R}`} is called the **least upper bound** or **supremum** of ${tex`A`}, if ${tex`u_0`} is an upper bound for ${tex`A`} (i.e. ${tex`\\forall a \\in A: \\; a \\leq u_0`}) and for all upper bounds ${tex`u`} of ${tex`A`} we have ${tex`u_0 \\leq u`}. We then denote ${tex`u_0 = \\sup A`}. \n\n> Let ${tex`B \\subset \\mathbb{R}`} be a nonempty subset (${tex`B \\neq \\emptyset`}) which is bounded from below. A number ${tex`\\ell_0 \\in \\mathbb{R}`} is called the **greatest lower bound** or **infimum** of ${tex`B`}, if ${tex`\\ell_0`} is a lower bound for ${tex`B`} (i.e. ${tex`\\forall b \\in B: \\; b \\geq \\ell_0`}) and for all lower bounds ${tex`\\ell`} of ${tex`B`} we have ${tex`\\ell_0 \\geq \\ell`}. We then denote ${tex`\\ell_0 = \\inf B`}. ","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":520,"value":"viewof sup_def_lean = nbFormulasEditor(sup_def_label, invalidation, { height: 60, header: html``})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":524,"value":"viewof inf_def_lean = nbFormulasEditor(inf_def_label, invalidation, { height: 60, header: html``})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":527,"value":"viewof sup_unique_lean = nbFormulasEditor(sup_unique_label, invalidation, { height: 60, header: html``})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":219,"value":"**Lemma II.29** (Characterization of supremum)\n\n> A number ${tex`u_0 \\in \\mathbb{R}`} is the supremum of a nonempty subset ${tex`A \\subset \\mathbb{R}`} which is bounded from above, if and only if the following two conditions hold: \n - For all ${tex`a \\in A`} we have ${tex`a \\leq u_0`};\n - For all ${tex`\\varepsilon>0`} there exists some ${tex`a \\in A`} such that ${tex`a > u_0 - \\varepsilon`}.","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":444,"value":"viewof sup_characterization_lean = nbFormulasEditor(sup_characterization_label, invalidation, { height: 60, header: html``})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":227,"value":"The **completeness axiom** of ${tex`\\mathbb{R}`} refers to any of the following (equivalent) statements: \n\n - (C1) Every non-empty subset ${tex`A \\subset \\mathbb{R}`} which is bounded from above has a least upper bound ${tex`\\sup A \\in \\mathbb{R}`}. \n\n - (C2) Every increasing real-number sequence ${tex`(a_n)_{n \\in \\mathbb{N}}`} which is bounded from above has a limit ${tex`\\lim_{n\\to \\infty} a_n \\in \\mathbb{R}`}. \n\n - (C3) Every collection ${tex`(I_n)_{n \\in \\mathbb{N}}`} of closed intervals ${tex`I_n \\subset \\mathbb{R}`}, which is nested in the sense that ${tex`I_{n+1} \\subset I_n`} for every ${tex`n \\in \\mathbb{N}`}, has a nonempty intersection ${tex.block`\\begin{aligned} \\bigcap_{n \\in \\mathbb{N}} I_n \\; \\neq \\; \\emptyset . \\end{aligned}`} \n","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":238,"value":"viewof completeness_axiom_C1_lean = nbFormulasEditor(completeness_axiom_C1_label, invalidation, { height: 60, header: html``})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":253,"value":"viewof completeness_axiom_C2_lean = nbFormulasEditor(completeness_axiom_C2_label, invalidation, { height: 60, header: html``})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":21,"value":"## Lean via tools by [@bryangingechen](https://observablehq.com/@bryangingechen)","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":11,"value":"leanLibName = \"library\"","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":6,"value":"import {leanEditor, leanEditorFrom, leanControl, leanHL, parseLeanMsgs} with {leanLibName} from '@bryangingechen/hello-lean-prover'","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":14,"value":"$4b","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":17,"value":"myFormulasEditor = leanEditorFrom({\n docArray: myFormulas,\n fileName: 'my_formulas.lean',\n readOnly: true,\n lineNumbers: false,\n height: 200,\n})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":233,"value":"inputleanfile = FileAttachment(\"metsp_obs_lean_02@3.lean\")","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":30,"value":"inputleancode = inputleanfile.text()","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":34,"value":"leanpieces = inputleancode.split('\\n-- ---\\n')","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":39,"value":"nbFormulasEditor = leanEditorFrom({\n docArray: leanpieces,\n fileName: 'metsp_ch00_pieces.lean',\n readOnly: false,\n lineNumbers: false,\n height: 400,\n})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":260,"value":"sup_unique_label = 25","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":269,"value":"inf_unique_label = 26","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":273,"value":"sup_characterization_label = 27","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":277,"value":"bounded_set_iff_label = 28","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":282,"value":"seq_upper_bound_label = 30","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":283,"value":"seq_lower_bound_label = 31","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":289,"value":"seq_bound_label = 32","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":295,"value":"seq_upper_bounded_label = 33","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":293,"value":"seq_lower_bounded_label = 34","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":299,"value":"seq_bounded_label = 35","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":242,"value":"completeness_axiom_C1_label = 65","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":245,"value":"completeness_axiom_C2_label = 66","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":309,"value":"seq_bounded_iff_both_label = 38","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":314,"value":"limit_label = 40","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":321,"value":"convergent_label = 41","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":326,"value":"limit_const_label = 42","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":330,"value":"preservation_ineq_label = 44","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":335,"value":"preservation_uppbd_label = 45","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":340,"value":"preservation_lowbd_label = 45","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":343,"value":"uniqueness_of_lim_label = 47","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":347,"value":"squeeze_label = 48","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":353,"value":"limit_sum_label = 51","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":356,"value":"limit_prod_label = 52","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":359,"value":"limit_quot_label = 53","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":365,"value":"limit_add_cst_label = 54","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":366,"value":"limit_mul_cst_label = 55","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":373,"value":"conv_imp_bdd_label = 56","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":393,"value":"alt_seq_divergent_label = 63","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":460,"value":"incr_label = 8","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":464,"value":"decr_label = 10","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":462,"value":"monotone_label = 12","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":470,"value":"incr_iff_label = 9","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":476,"value":"set_upbd_label = 14","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":483,"value":"set_upbdd_label = 16","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":477,"value":"set_lowbd_label = 15","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":485,"value":"set_lowbdd_label = 17","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":489,"value":"set_bdd_label = 18","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":493,"value":"sup_def_label = 19","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":496,"value":"inf_def_label = 21","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":502,"value":"max_def_label = 20","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":504,"value":"min_def_label = 22","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":508,"value":"max_is_sup_label = 23","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":512,"value":"min_is_inf_label = 24","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"}],"files":"$W4c","stdlib":"1"}} 24:null