31: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')32:[{"id":"9839c8f1d0e98f45a8b15e5f7ea75d93dfc5b4f6f957676c292824a7c2deb2e8d2e921753c636f9859197114b689a1d8b4242dc30835ee85ea3f5df01787c360","href":"https://static.observableusercontent.com/files/9839c8f1d0e98f45a8b15e5f7ea75d93dfc5b4f6f957676c292824a7c2deb2e8d2e921753c636f9859197114b689a1d8b4242dc30835ee85ea3f5df01787c360","name":"function-fig01.png","type":"image/png","lastModified":1641161500084.743,"size":79688},{"id":"06f523738cf723be7be2ec64e439268c8ee3c02aaf1ff7296a30a24a33c16376dc37f0fe7b85c2c458d577ed3ec387465678665ebad0403769467e03ddd6fd51","href":"https://static.observableusercontent.com/files/06f523738cf723be7be2ec64e439268c8ee3c02aaf1ff7296a30a24a33c16376dc37f0fe7b85c2c458d577ed3ec387465678665ebad0403769467e03ddd6fd51","name":"preimage-fig01.png","type":"image/png","lastModified":1641161277990.257,"size":125027},{"id":"f9adbe113e32f8b443187be81e6b34ecf8955be1f5c09d25a9de38daf374cfbb96f2327c916e0796577efab70d419204f487b38af003c45866d6f31da01d1724","href":"https://static.observableusercontent.com/files/f9adbe113e32f8b443187be81e6b34ecf8955be1f5c09d25a9de38daf374cfbb96f2327c916e0796577efab70d419204f487b38af003c45866d6f31da01d1724","name":"image-fig01.png","type":"image/png","lastModified":1641161290501.152,"size":109195},{"id":"034921a925c42d91434f9630f3904f64c48d9205bf51a0e88b6286e7b1a0f2124296595ef27e0ae23d3ff8a609e2d54922d0db7454b33f35af21e0e40ae3a695","href":"https://static.observableusercontent.com/files/034921a925c42d91434f9630f3904f64c48d9205bf51a0e88b6286e7b1a0f2124296595ef27e0ae23d3ff8a609e2d54922d0db7454b33f35af21e0e40ae3a695","name":"composition-fig01.png","type":"image/png","lastModified":1641158443598.805,"size":74891},{"id":"eeb8c60d72b76a7793c28af45710656e8877599961b7d2ae96ab6755d508bae069b98d8a7f1af243e9308c74351fb95fbf6b40e4471656a187b7fc9379ba944e","href":"https://static.observableusercontent.com/files/eeb8c60d72b76a7793c28af45710656e8877599961b7d2ae96ab6755d508bae069b98d8a7f1af243e9308c74351fb95fbf6b40e4471656a187b7fc9379ba944e","name":"metsp_obs_lean_01@10.lean","type":"application/octet-stream","lastModified":1641823351698.594,"size":8746}] 2f:{"title":"MetSp 2022 chapter 01: Foundations","cells":[{"id":0,"value":"# MetSp 2022 chapter 01: Foundations","pinned":false,"hidden":false,"mode":"md"},{"id":81,"value":"*This notebook is meant as supporting material for parts of Chapter I of the 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"},{"id":88,"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"},{"id":42,"value":"### Overview","pinned":false,"hidden":false,"mode":"md"},{"id":47,"value":"##### Key definitions:","pinned":false,"hidden":false,"mode":"md"},{"id":54,"value":"##### Key results:","pinned":false,"hidden":false,"mode":"md"},{"id":76,"value":"##### Key examples:","pinned":false,"hidden":false,"mode":"md"},{"id":60,"value":"##### Key ideas:","pinned":false,"hidden":false,"mode":"md"},{"id":64,"value":"# Today's math","pinned":false,"hidden":false,"mode":"md"},{"id":138,"value":"## Sets","pinned":false,"hidden":false,"mode":"md"},{"id":470,"value":"A few things to think about:\n\n * For any set ${tex`A`}, we have ${tex`\\emptyset \\subset A`}.\n * Whether ${tex`\\emptyset \\in A`} or ${tex`\\emptyset \\not\\in A`} depends on the set ${tex`A`}.\n * For example ${tex`\\emptyset \\not\\in \\N`}.\n * If ${tex`A`} denotes the set of all subsets of the plane, then we have ${tex`\\emptyset \\in A`}.\n * Does the empty set \"contain\" itself? Depends on whether \"contains\" means the set-membership relation \"${tex`\\in`}\" or the subset relation \"${tex`\\subset`}\"!\n * We have ${tex`\\emptyset \\subset \\emptyset`}.\n * We have ${tex`\\emptyset \\not\\in \\emptyset`}.\n * Perhaps it is best to avoid the word \"contain\", whose mathematical meaning is ambiguous (unless the context makes it clear which of the two relations it stands for).","pinned":false,"hidden":false,"mode":"md"},{"id":484,"value":"viewof emptyset_subset_lean = nbFormulasEditor(emptyset_subset_label, invalidation, { height: 30, header: html``})","pinned":false,"hidden":false,"mode":"ojs"},{"id":487,"value":"viewof emptyset_not_element_lean = nbFormulasEditor(emptyset_not_element_label, invalidation, { height: 30, header: html``})","pinned":false,"hidden":false,"mode":"ojs"},{"id":142,"value":"## Functions","pinned":false,"hidden":false,"mode":"md"},{"id":340,"value":"$${tex.block`f \\colon X \\to Y`}","pinned":false,"hidden":false,"mode":"md"},{"id":344,"value":"$${tex.block`x \\mapsto f(x)`}","pinned":false,"hidden":false,"mode":"md"},{"id":333,"value":"FileAttachment(\"function-fig01.png\").image()","pinned":false,"hidden":false,"mode":"ojs"},{"id":336,"value":" * ${tex`f`}: the name of our function\n * ${tex`X`}: the **domain** (of definition) of the function ${tex`f`}\n * the set of allowed arguments (\"input values\") of the function ${tex`f`}\n * ${tex`Y`}: the **codomain** of the function ${tex`f`}\n * the set of allowed values (\"output values\") of the function ${tex`f`}\n * to each argument ${tex`x \\in X`}, assign a value ${tex`f(x) \\in Y`}\n * denote ${tex`x \\mapsto f(x)`}, read \"${tex`x`} maps to ${tex`f(x)`}\"","pinned":false,"hidden":false,"mode":"md"},{"id":171,"value":"**Definition I.15** (Surjectivity, injectivity, and bijectivity)\n\n> Let ${tex`f \\colon X \\to Y`} be a function. ","pinned":false,"hidden":false,"mode":"md"},{"id":175,"value":"> We say that ${tex`f`} is **surjective** if for every ${tex`y \\in Y`} there exists an ${tex`x \\in X`} such that ${tex`y = f(x)`}. \n","pinned":false,"hidden":false,"mode":"md"},{"id":192,"value":"viewof surjective_def_lean = nbFormulasEditor(surjective_def_label, invalidation, { height: 20, header: html``})","pinned":false,"hidden":false,"mode":"ojs"},{"id":180,"value":"> We say that ${tex`f`} is **injective** if for any ${tex`x_1 , x_2 \\in X`} which are different, ${tex`x_1 \\neq x_2`}, also the corresponding function values are different, ${tex`f(x_1) \\neq f(x_2)`}. \n","pinned":false,"hidden":false,"mode":"md"},{"id":196,"value":"viewof injective_def_lean = nbFormulasEditor(injective_def_label, invalidation, { height: 20, header: html``})","pinned":false,"hidden":false,"mode":"ojs"},{"id":184,"value":"> We say that ${tex`f`} is **bijective** if it is both surjective and injective.","pinned":false,"hidden":false,"mode":"md"},{"id":213,"value":"viewof bijective_def_lean = nbFormulasEditor(bijective_def_label, invalidation, { height: 20, header: html``})","pinned":false,"hidden":false,"mode":"ojs"},{"id":223,"value":"**Exercise I.7** (Examples of injectivity and surjectivity)\n\n> Consider the functions\n - ${tex`f_1 \\colon \\mathbb{R}\\to \\mathbb{R}`} given by ${tex`f_1(x) = x^2`}\n - ${tex`f_2 \\colon \\mathbb{R}\\to [0,+\\infty)`} given by ${tex`f_2(x) = x^2`}\n - ${tex`f_3 \\colon [0,+\\infty) \\to \\mathbb{R}`} given by ${tex`f_3(x) = x^2`}\n - ${tex`f_4 \\colon (-\\infty,0] \\to \\mathbb{R}`} given by ${tex`f_4(x) = x^2`}\n - ${tex`f_5 \\colon (-\\infty,0] \\to [0,+\\infty)`} given by ${tex`f_5(x) = x^2`}\n\n> from Example I.14. Injective? Surjective? Bijective? Inverse function?","pinned":false,"hidden":false,"mode":"md"},{"id":237,"value":"### Compositions of functions\n\nSuppose that ${tex.block`\\begin{aligned} f \\colon X \\to Y \\qquad \\text{ and } \\qquad g \\colon Y \\to Z\\end{aligned}`} are two functions such that the codomain of ${tex`f`} is the same set as the domain of ${tex`g`} (both are ${tex`Y`}). Then we may form a new function, ${tex.block`\\begin{aligned} g \\circ f \\, \\colon \\, X \\to Z \\end{aligned}`} called the **composition** of ${tex`f`} and ${tex`g`} by the rule that at a point ${tex`x \\in X`} of its domain the value is ${tex.block`\\begin{aligned} \\big( g \\circ f \\big) (x) \\; = \\; g\\big(f(x)\\big) \\in Z .\\end{aligned}`}","pinned":false,"hidden":false,"mode":"md"},{"id":244,"value":"FileAttachment(\"composition-fig01.png\").image()","pinned":false,"hidden":false,"mode":"ojs"},{"id":247,"value":"**Exercise I.8** (Composition of injective functions is injective)\n\n> Show that if both ${tex`f \\colon X \\to Y`} and ${tex`g \\colon Y \\to Z`} are injective, then ${tex`g \\circ f \\colon X \\to Z`} is also injective. ","pinned":false,"hidden":false,"mode":"md"},{"id":310,"value":"viewof composition_of_injectives_lean = nbFormulasEditor(composition_of_injectives_label, invalidation, { height: 50, header: html``})","pinned":false,"hidden":false,"mode":"ojs"},{"id":251,"value":"**Exercise I.9** (Composition of surjective functions is surjective)\n\n> Show that if both ${tex`f \\colon X \\to Y`} and ${tex`g \\colon Y \\to Z`} are surjective, then ${tex`g \\circ f \\colon X \\to Z`} is also surjective. \n","pinned":false,"hidden":false,"mode":"md"},{"id":307,"value":"viewof composition_of_surjectives_lean = nbFormulasEditor(composition_of_surjectives_label, invalidation, { height: 50, header: html``})","pinned":false,"hidden":false,"mode":"ojs"},{"id":255,"value":"**Exercise I.10** (Injectivity of composition)\n\n> Let ${tex`f \\colon X \\to Y`} and ${tex`g \\colon Y \\to Z`} be functions such that ${tex`g \\circ f \\colon X \\to Z`} is injective. \n - Show that ${tex`f`} is also injective. \n - Construct an example which shows that ${tex`g`} does not have to be injective.","pinned":false,"hidden":false,"mode":"md"},{"id":304,"value":"viewof injectivity_of_composition_lean = nbFormulasEditor(injectivity_of_composition_label, invalidation, { height: 50, header: html``})","pinned":false,"hidden":false,"mode":"ojs"},{"id":259,"value":"**Exercise I.10** (Surjectivity of composition)\n\n> Let ${tex`f \\colon X \\to Y`} and ${tex`g \\colon Y \\to Z`} be functions such that ${tex`g \\circ f \\colon X \\to Z`} is surjective. \n - Show that ${tex`g`} is also surjective. \n - Construct an example which shows that ${tex`f`} does not have to be surjective.","pinned":false,"hidden":false,"mode":"md"},{"id":301,"value":"viewof surjectivity_of_composition_lean = nbFormulasEditor(surjectivity_of_composition_label, invalidation, { height: 50, header: html``})","pinned":false,"hidden":false,"mode":"ojs"},{"id":264,"value":"### Images and preimages under functions\n\nLet ${tex`f \\colon X \\to Y`} be a function. ","pinned":false,"hidden":false,"mode":"md"},{"id":322,"value":"FileAttachment(\"image-fig01.png\").image()","pinned":false,"hidden":false,"mode":"ojs"},{"id":275,"value":"If ${tex`A \\subset X`} is a subset of the domain of ${tex`f`}, then the **image** of ${tex`A`} under ${tex`f`} is the subset ${tex.block`\\begin{aligned} f[A] \\; = \\;\\; & \\left\\{ f(a) \\; \\big| \\; a \\in A \\right\\}\n\\; = \\; \\left\\{ y \\in Y \\; \\big| \\; \\exists a \\in A, \\; y = f(a) \\right\\} \\end{aligned}`} of the codomain of ${tex`f`} consisting of those points ${tex`y \\in Y`} which are obtained as the value at some point ${tex`a \\in A \\subset X`}, i.e., ${tex`y = f(a)`}. ","pinned":false,"hidden":false,"mode":"md"},{"id":326,"value":"FileAttachment(\"preimage-fig01.png\").image()","pinned":false,"hidden":false,"mode":"ojs"},{"id":269,"value":"If ${tex`B \\subset Y`} is a subset of the codomain of ${tex`f`}, then the **preimage** of ${tex`B`} under ${tex`f`} is the subset ${tex.block`\\begin{aligned} f^{-1}[B] \\; = \\;\\; & \\left\\{ x \\in X \\; \\big| \\; f(x) \\in B \\right\\} \\end{aligned}`} of the domain of ${tex`f`} consisting of those points ${tex`x \\in X`} at which the value belongs to the subset ${tex`B \\subset Y`}. The notation ${tex`f^{-1}`} is used for both the inverse function and the preimage, but we try to consistently use square brackets in the latter case. The inverse function only exists if ${tex`f`} is a bijection, whereas preimages are always defined. \n","pinned":false,"hidden":false,"mode":"md"},{"id":146,"value":"## Logic","pinned":false,"hidden":false,"mode":"md"},{"id":288,"value":"### Quantifiers\n\n * **universal quantifier**: ${tex`\\forall`} (read as \"for all ...\") \n * **existential quantifier**: ${tex`\\exists`} (read as \"there exists ...\")","pinned":false,"hidden":false,"mode":"md"},{"id":293,"value":"The order of quantifiers matters! Consider the two statements ${tex.block`\\forall n \\in \\Z \\quad \\exists m \\in \\Z \\quad m < n`} ${tex.block`\\exists m \\in \\Z \\quad \\forall n \\in \\Z \\quad m < n .`}\nOne of the above statements is correct whereas the other one is incorrect!","pinned":false,"hidden":false,"mode":"md"},{"id":348,"value":"viewof order_of_quantifiers_A_lean = nbFormulasEditor(order_of_quantifiers_A_label, invalidation, { height: 30, header: html``})","pinned":false,"hidden":false,"mode":"ojs"},{"id":393,"value":"viewof order_of_quantifiers_B_lean = nbFormulasEditor(order_of_quantifiers_B_label, invalidation, { height: 30, header: html``})","pinned":false,"hidden":false,"mode":"ojs"},{"id":156,"value":"### Contrapositives\n\nThe implications ${tex.block`\\begin{aligned} P \\;\\;\\Longrightarrow \\;\\; & Q \\\\ \\neg\\,{Q} \\;\\;\\Longrightarrow \\;\\; & \\neg\\,{P}\\end{aligned}`} are logically equivalent — you should make sure that you understand why. The second implication is known as the **contrapositive** of the first.","pinned":false,"hidden":false,"mode":"md"},{"id":150,"value":" **Example I.32** (Revisiting injectivity)\n \n> Recall definition of an injective function ${tex`f \\colon X \\to Y`} from Definition I.15. In logical symbols, injectivity means ${tex.block`\\begin{aligned} \\forall \\, x_1 , x_2 \\in X \\qquad x_1 \\neq x_2 \\; \\Longrightarrow \\; f(x_1) \\neq f(x_2).\\end{aligned}`} An equivalent form of this condition can be obtained by taking a contrapositive of the implication above. This is particularly helpful, since the contrapositive will involve negations of the propositions ${tex`x_1 \\neq x_2`} and ${tex`f(x_1) \\neq f(x_2)`}, which are simply ${tex`x_1 = x_2`} and ${tex`f(x_1) = f(x_2)`}, respectively. Using the contrapositive form, we find that injectivity equivalently means ${tex.block`\\begin{aligned} \\forall \\, x_1 , x_2 \\in X \\qquad f(x_1) = f(x_2) \\; \\Longrightarrow \\; x_1 = x_2 .\\end{aligned}`} \n","pinned":false,"hidden":false,"mode":"md"},{"id":353,"value":"viewof contrapositive_injectivity_lean = nbFormulasEditor(contrapositive_injectivity_label, invalidation, { height: 60, header: html``})","pinned":false,"hidden":false,"mode":"ojs"},{"id":21,"value":"# Lean via tools by [@bryangingechen](https://observablehq.com/@bryangingechen)","pinned":false,"hidden":false,"mode":"md"},{"id":11,"value":"leanLibName = \"library\"","pinned":false,"hidden":false,"mode":"ojs"},{"id":6,"value":"import {leanEditor, leanEditorFrom, leanControl, leanHL, parseLeanMsgs} with {leanLibName} from '@bryangingechen/hello-lean-prover'","pinned":false,"hidden":false,"mode":"ojs"},{"id":14,"value":"$31","pinned":false,"hidden":false,"mode":"ojs"},{"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"},{"id":377,"value":"inputleanfile = FileAttachment(\"metsp_obs_lean_01@10.lean\")","pinned":false,"hidden":false,"mode":"ojs"},{"id":30,"value":"inputleancode = inputleanfile.text()","pinned":false,"hidden":false,"mode":"ojs"},{"id":34,"value":"leanpieces = inputleancode.split('\\n-- ---\\n')","pinned":false,"hidden":false,"mode":"ojs"},{"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"},{"id":199,"value":"injective_def_label = 5","pinned":false,"hidden":false,"mode":"ojs"},{"id":202,"value":"surjective_def_label = 3","pinned":false,"hidden":false,"mode":"ojs"},{"id":205,"value":"bijective_def_label = 7","pinned":false,"hidden":false,"mode":"ojs"},{"id":371,"value":"composition_of_injectives_label = 10","pinned":false,"hidden":false,"mode":"ojs"},{"id":367,"value":"composition_of_surjectives_label = 16","pinned":false,"hidden":false,"mode":"ojs"},{"id":365,"value":"injectivity_of_composition_label = 12","pinned":false,"hidden":false,"mode":"ojs"},{"id":362,"value":"surjectivity_of_composition_label = 18","pinned":false,"hidden":false,"mode":"ojs"},{"id":359,"value":"order_of_quantifiers_A_label = 22","pinned":false,"hidden":false,"mode":"ojs"},{"id":397,"value":"order_of_quantifiers_B_label = 24","pinned":false,"hidden":false,"mode":"ojs"},{"id":356,"value":"contrapositive_injectivity_label = 20","pinned":false,"hidden":false,"mode":"ojs"},{"id":437,"value":"fillintheblank1a_label = 26","pinned":false,"hidden":false,"mode":"ojs"},{"id":451,"value":"fillintheblank1b_label = 27","pinned":false,"hidden":false,"mode":"ojs"},{"id":478,"value":"emptyset_subset_label = 29","pinned":false,"hidden":false,"mode":"ojs"},{"id":481,"value":"emptyset_not_element_label = 30","pinned":false,"hidden":false,"mode":"ojs"}],"files":"$W32","stdlib":"1","titling":"auto"}