Search.setIndex({"docnames": ["C01_Introduction", "C02_Basics", "C03_Logic", "C04_Sets_and_Functions", "C05_Number_Theory", "C06_Abstract_Algebra", "C07_Topology", "C08_Differential_Calculus", "C09_Integration_and_Measure_Theory", "genindex", "index"], "filenames": ["C01_Introduction.rst", "C02_Basics.rst", "C03_Logic.rst", "C04_Sets_and_Functions.rst", "C05_Number_Theory.rst", "C06_Abstract_Algebra.rst", "C07_Topology.rst", "C08_Differential_Calculus.rst", "C09_Integration_and_Measure_Theory.rst", "genindex.rst", "index.rst"], "titles": ["<span class=\"section-number\">1. </span>Introduction", "<span class=\"section-number\">2. </span>Basics", "<span class=\"section-number\">3. </span>Logic", "<span class=\"section-number\">4. </span>Sets and Functions", "<span class=\"section-number\">5. </span>Number Theory", "<span class=\"section-number\">6. </span>Abstract Algebra", "<span class=\"section-number\">7. </span>Topology", "Differential Calculus", "Integration and Measure Theory", "Index", "Mathematics in Lean"], "terms": {"The": [0, 1, 4, 5, 6, 10], "goal": [0, 1, 2, 3, 4, 5, 6], "thi": [0, 1, 2, 3, 4, 5, 6, 7], "book": [0, 6], "teach": 0, "you": [0, 1, 2, 3, 4, 5, 6], "formal": [0, 1, 2, 3, 4, 5, 6, 7], "mathemat": [0, 1, 2, 3, 4, 5, 6], "us": [0, 2, 3, 4, 5, 6, 10], "lean": [0, 1, 2, 3, 4, 5, 6], "4": [0, 1, 2, 4, 5, 6], "interact": [0, 5], "proof": [0, 1, 2, 3, 4, 5, 6], "assist": [0, 5], "It": [0, 1, 2, 3, 4, 5, 6], "assum": [0, 1, 2, 3, 4, 6], "know": [0, 1, 2, 3, 4, 5, 6], "some": [0, 1, 2, 3, 4, 5, 6], "doe": [0, 1, 2, 3, 4, 5, 6], "requir": [0, 1, 2, 3, 4, 5, 6], "much": [0, 2, 4, 6, 7], "although": [0, 3, 4, 5, 6], "we": [0, 1, 2, 3, 4, 5, 6, 7], "cover": [0, 1, 3, 6], "exampl": [0, 1, 2, 3, 4, 5, 6], "rang": [0, 2, 3, 4, 6], "from": [0, 1, 2, 3, 4, 5, 6, 7], "number": [0, 1, 2, 3, 5, 6, 7, 10], "theori": [0, 1, 2, 3, 6, 7, 10], "measur": [0, 5, 6, 7], "analysi": [0, 5, 7], "focu": [0, 1, 6], "elementari": [0, 3, 4, 5, 6], "aspect": [0, 5], "those": [0, 1, 2, 3, 5, 6], "field": [0, 1, 5], "hope": 0, "thei": [0, 1, 2, 3, 4, 5, 6], "ar": [0, 1, 2, 3, 4, 5, 6], "familiar": [0, 1, 4, 5, 6, 7], "can": [0, 1, 2, 3, 4, 5, 6], "pick": 0, "them": [0, 1, 2, 3, 4, 5, 6], "up": [0, 2, 3, 4, 5, 6], "go": [0, 1, 2, 3, 4, 6], "also": [0, 1, 2, 3, 4, 5, 6], "don": [0, 1, 2, 3, 4, 5, 6], "t": [0, 1, 2, 3, 4, 5, 6], "presuppos": 0, "ani": [0, 1, 2, 3, 4, 5, 6, 7], "background": 0, "seen": [0, 1, 2, 4, 5, 6], "kind": [0, 1, 6], "comput": [0, 3, 4, 5], "program": [0, 1], "write": [0, 1, 2, 3, 4, 5, 6], "definit": [0, 1, 2, 3, 4, 5, 6], "theorem": [0, 2, 4, 5, 6, 10], "regiment": 0, "languag": [0, 1, 3], "like": [0, 1, 2, 3, 4, 5, 6], "understand": [0, 2, 3, 4, 5, 6], "In": [0, 1, 2, 3, 4, 5, 6, 7], "return": [0, 2, 3, 4, 5, 6], "provid": [0, 1, 2, 3, 4, 5, 6], "feedback": 0, "inform": [0, 1, 2, 3, 5, 6], "interpret": [0, 1, 4, 5, 6], "express": [0, 1, 2, 3, 4, 5, 6], "guarante": [0, 3, 5], "well": [0, 1, 2, 3, 4, 5, 6], "form": [0, 1, 2, 3, 4, 5, 6], "ultim": 0, "certifi": 0, "correct": [0, 1], "our": [0, 1, 2, 3, 4, 5, 6], "learn": [0, 1, 2, 4, 5], "more": [0, 2, 3, 4, 5, 6, 10], "about": [0, 2, 3, 4, 5, 6, 10], "project": [0, 4, 5, 6], "page": [0, 1, 4], "commun": [0, 4], "web": [0, 1, 4], "tutori": 0, "base": [0, 3, 4, 6], "s": [0, 1, 2, 3, 4, 5, 6], "larg": [0, 6], "ever": [0, 6], "grow": 0, "librari": [0, 1, 2, 3, 4, 5, 6], "mathlib": [0, 1, 2, 3, 4, 5, 6], "strongli": 0, "recommend": [0, 1, 3], "take": [0, 1, 2, 3, 4, 5, 6], "look": [0, 1, 2, 3, 4, 6], "zulip": [0, 4], "onlin": 0, "chat": 0, "group": [0, 1, 2, 3, 5, 6], "haven": [0, 2, 6], "alreadi": [0, 1, 2, 3, 4, 5, 6], "ll": [0, 1, 2, 4, 6], "find": [0, 1, 2, 4, 5, 6], "live": [0, 5], "welcom": [0, 1], "enthusiast": 0, "happi": 0, "answer": [0, 5, 6], "question": [0, 4, 6], "offer": [0, 2, 5, 6], "moral": [0, 5], "support": [0, 1, 2, 3, 4, 5, 6], "read": [0, 1, 4, 6], "pdf": 0, "html": 0, "version": [0, 1, 2, 3, 4, 5, 6], "design": [0, 1, 2, 3, 5, 6], "run": 0, "insid": [0, 1, 2, 3], "vs": [0, 1, 2, 3, 5], "code": [0, 1, 2, 3, 5], "editor": [0, 1], "To": [0, 1, 2, 3, 4, 5, 6], "instal": 0, "follow": [0, 1, 2, 3, 4, 5, 6], "instruct": [0, 1, 6], "http": 0, "github": [0, 1], "com": 0, "leanprov": 0, "lean4": 0, "blob": 0, "master": [0, 1, 4], "doc": 0, "quickstart": 0, "md": 0, "_": [0, 1, 2, 3, 4, 5, 6], "termin": 0, "navig": 0, "folder": 0, "where": [0, 1, 2, 3, 4, 5, 6], "want": [0, 1, 2, 3, 4, 5, 6], "put": [0, 1, 2, 3, 4, 5, 6], "copi": [0, 3, 4, 6], "repositori": [0, 1], "type": [0, 1, 2, 3, 4, 5, 6], "git": 0, "clone": 0, "mathematics_in_lean": 0, "fetch": 0, "execut": 0, "lake": 0, "ex": [0, 2], "cach": 0, "compil": 0, "open": [0, 1, 2, 3, 4, 5], "altern": [0, 2, 3, 4, 5, 6], "choos": [0, 2, 3, 4, 5, 6], "file": [0, 1, 4, 5, 6], "menu": [0, 1], "Be": [0, 1, 3], "sure": [0, 1, 2, 3, 5], "other": [0, 1, 2, 3, 4, 5, 6], "simultan": 0, "window": [0, 1, 2, 5], "updat": 0, "newer": 0, "ty": 0, "pull": [0, 6], "cloud": 0, "gitpod": 0, "how": [0, 1, 2, 3, 4, 5, 6], "do": [0, 1, 2, 3, 4, 5, 6], "each": [0, 1, 2, 3, 4, 5, 6], "section": [0, 1, 2, 3, 4, 5, 6], "ha": [0, 1, 2, 3, 4, 5, 6], "an": [0, 1, 2, 3, 4, 5, 6], "associ": [0, 1, 2, 4, 5, 6], "exercis": [0, 1, 2, 3, 5, 6], "src": 0, "organ": 0, "chapter": [0, 1, 2, 3, 4, 5, 6, 7], "make": [0, 1, 2, 3, 4, 5, 6], "so": [0, 1, 2, 3, 4, 5, 6], "experi": [0, 1, 6], "while": [0, 1, 2, 6], "leav": [0, 1, 2, 3, 5], "origin": [0, 1, 5], "intact": 0, "text": [0, 3, 5, 6], "often": [0, 1, 2, 3, 4, 5, 6], "includ": [0, 1, 2, 3, 4, 6], "one": [0, 1, 2, 3, 4, 5, 6], "eval": 0, "hello": 0, "world": 0, "should": [0, 1, 2, 3, 4, 5, 6], "abl": [0, 1, 2, 3, 4, 5], "correspond": [0, 1, 2, 3, 4, 5, 6], "If": [0, 1, 2, 3, 4, 5, 6], "click": [0, 1, 3, 4, 5], "line": [0, 1, 2, 3, 4], "show": [0, 1, 2, 3, 4, 5, 6], "hover": [0, 1, 2, 3, 4, 5], "your": [0, 1, 2, 3, 5, 6], "cursor": [0, 1, 2], "over": [0, 1, 2, 3, 4, 5, 6], "command": [0, 1, 2, 3, 4, 5], "respons": [0, 1], "pop": 0, "encourag": [0, 1, 2, 3, 4, 5], "edit": 0, "try": [0, 1, 2, 3, 4, 5, 6], "own": [0, 1, 4, 5], "moreov": [0, 1, 4, 5, 6], "lot": [0, 3, 5, 6], "challeng": [0, 1, 2, 3, 5], "rush": 0, "past": [0, 1], "just": [0, 1, 2, 3, 4, 5, 6], "work": [0, 1, 2, 3, 4, 5, 6], "through": [0, 1, 3, 4, 5, 6], "central": [0, 4], "alwai": [0, 1, 2, 3, 5], "compar": [0, 5, 6], "solut": [0, 1, 4], "ones": [0, 1, 2, 3, 5], "simpli": [0, 1, 2, 3, 4, 5, 6], "tool": [0, 1, 2, 5], "build": [0, 2, 4, 6, 10], "complex": [0, 1, 2, 4, 5], "known": [0, 1, 2, 3, 4, 5, 6], "depend": [0, 2, 3, 4, 5, 6], "everi": [0, 1, 2, 3, 4, 5, 6], "check": [0, 1, 2, 3, 4, 5, 6], "print": [0, 3, 4, 5], "have": [0, 1, 2, 3, 4, 5, 6], "\u2115": [0, 1, 2, 3, 4, 5, 6], "These": [0, 1, 2, 3, 4, 5], "object": [0, 1, 2, 3, 4, 5], "2": [0, 1, 2, 3, 4, 5, 6], "def": [0, 2, 3, 4, 5, 6], "f": [0, 1, 2, 3, 4, 5, 6], "x": [0, 1, 2, 3, 4, 5, 6], "3": [0, 1, 2, 3, 4, 5, 6], "prop": [0, 2, 3, 4, 5, 6], "statement": [0, 1, 2, 3, 4, 5, 6], "fermatlasttheorem": 0, "y": [0, 1, 2, 3, 4, 5, 6], "z": [0, 1, 2, 5, 6], "n": [0, 1, 2, 3, 4, 5, 6], "0": [0, 1, 2, 3, 4, 5, 6], "p": [0, 2, 3, 4, 5, 6], "itself": [0, 3, 5, 6], "Such": [0, 1, 2], "proposit": [0, 2, 3, 4, 5], "easi": [0, 4, 5, 6], "rfl": [0, 1, 2, 3, 4, 5, 6], "hard": [0, 1, 3, 5], "sorri": [0, 1, 2, 3, 4, 5, 6], "manag": [0, 1, 4, 5, 6], "construct": [0, 2, 3, 4, 5, 6], "fermat_last_theorem": 0, "accept": [0, 1, 6], "term": [0, 1, 2, 3, 4, 5, 6], "done": [0, 2, 3, 4, 6], "someth": [0, 1, 2, 4, 6], "veri": [0, 2, 4, 6], "impress": 0, "cheat": [0, 1], "now": [0, 1, 2, 3, 4, 5, 6, 7], "game": 0, "all": [0, 1, 2, 3, 4, 5, 6], "left": [0, 1, 2, 3, 4, 5, 6], "rule": [0, 2, 4, 5, 6], "complementari": 0, "companion": [0, 1], "prove": [0, 2, 3, 4, 5, 6, 10], "which": [0, 1, 2, 3, 4, 5, 6, 7], "thorough": 0, "underli": [0, 1, 5], "logic": [0, 1, 3, 4, 5, 10], "framework": 0, "core": [0, 4, 5], "syntax": [0, 1, 3, 4], "peopl": [0, 1], "who": [0, 6], "prefer": [0, 1, 3], "user": [0, 2], "manual": [0, 3, 4], "befor": [0, 1, 2, 3, 4, 5], "new": [0, 1, 2, 3, 4, 5, 6], "dishwash": 0, "person": 0, "hit": [0, 1], "button": [0, 1], "figur": [0, 1, 2, 5], "out": [0, 1, 2, 3, 4, 5, 6], "activ": 0, "potscrubb": 0, "featur": [0, 1, 2, 4], "later": [0, 1, 2, 4, 5, 6], "sens": [0, 2, 3, 4, 5, 6], "here": [0, 1, 2, 3, 4, 5, 6], "refer": [0, 1, 2, 4, 5, 6], "back": [0, 1, 2, 3, 5, 6], "necessari": [0, 2, 4, 5], "anoth": [0, 1, 2, 3, 4, 5, 6], "thing": [0, 1, 2, 3, 4, 5, 6], "distinguish": [0, 5, 6], "place": [0, 1, 2, 5, 6], "greater": [0, 1, 2, 3, 4, 6], "emphasi": 0, "tactic": [0, 1, 2, 3, 4, 5, 6], "given": [0, 1, 2, 3, 4, 5, 6], "two": [0, 1, 2, 3, 4, 5, 6], "wai": [0, 1, 2, 3, 4, 5, 6], "down": [0, 3, 4, 6], "themselv": [0, 4, 5], "suitabl": [0, 1, 2, 5, 6], "descript": [0, 1, 2, 4, 6], "thereof": 0, "For": [0, 1, 2, 3, 4, 5, 6], "repres": [0, 1, 2, 3, 4, 5], "fact": [0, 2, 3, 4, 5, 6, 10], "even": [0, 1, 2, 3, 4, 5, 6], "m": [0, 1, 2, 4, 6], "nat": [0, 1, 2, 3, 4, 5, 6], "fun": [0, 2, 3, 4, 5, 6], "k": [0, 2, 4, 5, 6], "hk": 0, "hmn": 0, "rw": [0, 1, 2, 3, 4, 5, 6], "mul_add": [0, 1, 4], "l": [0, 1], "compress": [0, 1, 6], "singl": [0, 1, 2, 3, 4, 5], "instead": [0, 1, 2, 3, 4, 5, 6], "style": [0, 1], "same": [0, 1, 2, 3, 4, 5, 6], "sai": [0, 1, 2, 3, 4, 5, 6], "natur": [0, 1, 2, 3, 4, 5, 6], "rintro": [0, 2, 3, 4, 5, 6], "need": [0, 1, 2, 3, 4, 5, 6], "twice": [0, 6], "let": [0, 1, 2, 3, 4, 5, 6], "substitut": [0, 2], "obviou": [0, 4, 5], "ring": [0, 1, 2, 3, 4, 5], "As": [0, 1, 2, 3, 4, 5, 6], "enter": [0, 1, 2, 3, 6], "displai": [0, 1, 2], "state": [0, 1, 2, 3, 4, 6], "separ": [0, 1, 2, 4, 5], "tell": [0, 2, 3, 4, 5], "what": [0, 1, 2, 3, 4, 5, 6], "establish": [0, 1, 2, 3, 4, 5], "task": [0, 2, 4, 5, 6], "remain": [0, 1, 2, 3, 5, 6], "replai": 0, "step": [0, 1, 2, 3, 4, 5], "sinc": [0, 1, 2, 3, 4, 5, 6], "continu": [0, 1, 4, 5], "point": [0, 1, 2, 3, 5, 6], "see": [0, 1, 2, 3, 4, 5, 6], "first": [0, 1, 2, 3, 4, 5, 6], "introduc": [0, 1, 2, 3, 4, 6], "could": [0, 1, 2, 4, 5, 6], "renam": 0, "decompos": [0, 3, 5], "hypothesi": [0, 1, 2, 3, 4], "assumpt": [0, 1, 2, 3, 4, 5, 6], "second": [0, 1, 2, 3, 4, 5, 6], "declar": [0, 1, 4, 5], "next": [0, 1, 2, 3, 4, 5, 6, 7], "rewrit": [0, 1, 2, 3, 4, 5, 6], "replac": [0, 1, 2, 3, 4], "solv": [0, 1, 2, 3, 4, 5, 6], "result": [0, 1, 2, 3, 4, 5, 6], "abil": 0, "small": [0, 4, 5, 6], "increment": [0, 1], "extrem": [0, 6], "power": [0, 2, 3, 4, 5], "reason": [0, 1, 2, 4, 5, 6], "easier": [0, 1, 3, 4, 6], "quicker": 0, "than": [0, 1, 2, 3, 4, 5, 6], "There": [0, 1, 2, 3, 4, 6], "isn": [0, 2, 3, 4], "sharp": 0, "distinct": [0, 2, 3, 4, 5, 6], "between": [0, 1, 2, 3, 4, 5, 6], "insert": [0, 2, 4, 5, 6], "did": [0, 2, 6], "phrase": [0, 1, 2, 4, 5], "mul_left_comm": [0, 4], "abov": [0, 1, 2, 3, 4, 5, 6], "convers": [0, 1, 2, 4, 6], "short": [0, 1, 2, 3, 4, 5], "middl": [0, 1, 2, 6], "That": [0, 4, 5], "said": [0, 2, 4, 5], "reduc": [0, 2, 3, 4, 5], "liner": 0, "carri": [0, 1, 2, 3, 4, 5, 6], "But": [0, 1, 2, 3, 4, 5, 6], "substanti": 0, "autom": [0, 1, 5], "justifi": [0, 1, 2, 6], "longer": [0, 4, 5], "calcul": [0, 2, 4, 5, 10], "bigger": [0, 3], "inferenti": 0, "invok": [0, 1, 6], "simplifi": [0, 2, 3, 4, 5, 6], "specif": [0, 1, 3, 4, 5], "pariti": [0, 4], "automat": [0, 1, 2, 3, 4, 5, 6], "intro": [0, 1, 2, 3, 4, 5, 6], "simp": [0, 2, 3, 4, 5, 6], "parity_simp": 0, "big": [0, 5, 6], "differ": [0, 1, 2, 3, 4, 5, 6], "onli": [0, 1, 2, 3, 4, 5, 6], "its": [0, 1, 2, 3, 4, 5, 6], "built": [0, 2], "wherea": [0, 1, 3, 5, 6], "top": [0, 6], "meant": [0, 1, 2], "contain": [0, 2, 3, 4, 5, 6], "extens": [0, 1, 6], "document": [0, 1, 3, 4], "rather": [0, 1, 2, 4, 5, 6], "think": [0, 1, 2, 3, 4, 5, 6], "comfort": [0, 2], "brows": [0, 1, 4], "frustrat": 0, "curv": 0, "steep": 0, "newcom": 0, "avail": [0, 4, 5], "round": [0, 1, 5], "clock": 0, "doubt": 0, "soon": [0, 2, 6], "enough": [0, 1, 2, 3, 4, 6], "too": [0, 1, 3, 5, 6], "contribut": [0, 3], "develop": [0, 1, 4], "mission": 0, "dive": 0, "come": [0, 1, 2, 3, 4, 5, 6], "forewarn": 0, "fundament": [0, 4, 5], "life": [0, 2], "mai": [0, 1, 2, 3, 5, 6], "never": 0, "acknowledg": 0, "grate": [0, 5], "gabriel": 0, "ebner": 0, "set": [0, 1, 2, 4, 5, 7, 10], "infrastructur": 0, "scott": 0, "morrison": 0, "mario": 0, "carneiro": 0, "help": [0, 1, 2, 3, 4, 5, 6], "port": 0, "bryan": 0, "gin": 0, "ge": [0, 2, 5], "chen": 0, "johan": 0, "commelin": 0, "mathieu": 0, "guai": 0, "paquet": 0, "julian": 0, "k\u00fclshammer": 0, "giovanni": 0, "mascellani": 0, "hunter": 0, "monro": 0, "pietro": 0, "monticon": 0, "bartosz": 0, "piotrowski": 0, "guilherm": 0, "silva": 0, "been": [0, 1, 2, 4, 5], "partial": [0, 1, 2, 3, 5], "hoskinson": 0, "center": [0, 6], "nut": 1, "bolt": 1, "appli": [1, 2, 3, 4, 5, 6], "gener": [1, 2, 3, 4, 5, 6], "without": [1, 2, 4, 5, 6], "when": [1, 2, 3, 4, 5, 6], "net": 1, "hand": [1, 2, 3, 4, 5, 6], "side": [1, 2, 3, 4, 5, 6], "equal": [1, 2, 3, 4, 5, 6], "right": [1, 2, 3, 4, 5, 6], "tantamount": [1, 3], "name": [1, 2, 3, 4, 5, 6], "abbrevi": [1, 2, 3, 5], "b": [1, 2, 3, 4, 5, 6], "c": [1, 2, 4, 5, 6], "real": [1, 2, 3, 4, 5, 6, 7], "mul_assoc": [1, 2, 4, 5], "mul_comm": [1, 2, 4, 5], "elimin": 1, "explicitli": [1, 2, 3, 5, 6], "purpos": [1, 2, 3, 4, 5, 6], "illustr": [1, 2, 3, 4, 5], "multipl": [1, 2, 3, 4, 5], "written": [1, 2, 3, 4, 5, 6], "howev": [1, 2, 5, 6], "good": [1, 2, 3, 4, 5, 6], "mind": [1, 2, 5], "notat": [1, 2, 3, 4, 5, 6], "convent": [1, 5], "parenthes": [1, 2, 3, 4], "\u211d": [1, 2, 3, 5, 6], "import": [1, 2, 3, 4, 5, 6], "begin": [1, 2, 3, 4, 5], "sake": [1, 4], "breviti": [1, 5], "suppress": 1, "repeat": [1, 4, 5], "full": [1, 3, 4, 5, 6], "process": [1, 3], "chang": [1, 2, 4, 5, 6], "happen": [1, 6], "charact": [1, 3], "r": [1, 2, 4, 5, 6], "symbol": [1, 2, 5], "doesn": [1, 2, 6], "appear": [1, 2, 5, 6], "until": [1, 2, 4, 5, 6], "space": [1, 3, 5, 10], "tab": [1, 2, 3, 4], "kei": [1, 4, 5, 6], "keyboard": 1, "easili": [1, 4, 5], "access": [1, 3, 5, 6], "backslash": [1, 3], "lead": [1, 2, 4, 5, 6], "input": [1, 3, 6], "leader": 1, "report": 1, "current": [1, 2], "infoview": 1, "move": [1, 2, 6], "A": [1, 2, 3, 4, 5, 6], "typic": 1, "might": [1, 2, 3, 4, 5], "1": [1, 2, 3, 4, 5, 6], "h\u2081": [1, 2, 3, 4], "prime": [1, 2, 3, 5, 10], "h\u2082": [1, 3, 4], "h\u2083": [1, 3], "denot": [1, 3, 4, 6], "context": [1, 2, 4, 5, 6], "plai": [1, 3, 4, 6], "three": [1, 2, 4, 5, 6], "label": [1, 2], "everyth": [1, 2, 6], "identifi": [1, 2, 4], "subscript": 1, "h": [1, 2, 3, 4, 5, 6], "legal": 1, "would": [1, 2, 3, 4, 5, 6], "h1": [1, 3, 4], "h2": [1, 3], "h3": 1, "foo": [1, 3, 5], "bar": [1, 2], "baz": 1, "last": [1, 2, 3, 4, 5, 6], "sometim": [1, 2, 3, 4, 5, 6], "target": [1, 6], "combin": [1, 2, 5, 6], "practic": [1, 2, 3, 6], "intend": [1, 2, 5], "mean": [1, 2, 3, 4, 5, 6], "usual": [1, 2, 3, 4, 5, 6], "clear": [1, 2, 4, 5], "case": [1, 2, 3, 4, 5, 6], "With": [1, 3, 4, 6], "arrow": [1, 2, 6], "revers": [1, 2, 3, 5, 6], "argument": [1, 2, 3, 4, 5, 6], "tri": [1, 2, 4], "match": [1, 2, 5], "pattern": [1, 2, 3, 5], "local": [1, 2, 6], "d": [1, 2, 4, 5], "e": [1, 2, 3, 4, 5, 6], "hyp": 1, "sub_self": [1, 2], "list": [1, 2, 3, 4, 5], "relev": [1, 2, 4, 5, 6], "within": [1, 2, 6], "squar": [1, 2, 4, 5], "bracket": [1, 2, 5], "still": [1, 2, 3, 4, 5, 6], "progress": [1, 5], "after": [1, 2, 4, 6], "comma": 1, "trick": [1, 2, 4], "variabl": [1, 2, 3, 4, 5, 6], "onc": [1, 2, 3, 4, 5, 6], "outsid": [1, 4], "mention": [1, 2, 3, 5, 6], "g": [1, 2, 3, 5, 6], "inspect": 1, "reveal": 1, "inde": [1, 5, 6], "delimit": 1, "scope": [1, 2, 3, 5], "end": [1, 2, 3, 4, 5, 6], "block": [1, 4], "final": [1, 2, 3, 5, 6], "recal": [1, 2, 4, 5, 6], "introduct": [1, 2, 6, 10], "determin": [1, 5, 6], "both": [1, 2, 3, 4, 5, 6], "expect": [1, 2, 3, 4, 5, 6], "rais": [1, 4], "error": [1, 2, 3], "explain": [1, 2, 3, 4, 5, 6], "output": 1, "meanwhil": [1, 4], "two_mul": [1, 5], "add_mul": 1, "distribut": [1, 4, 5], "addit": [1, 2, 4, 5, 6], "add_assoc": [1, 4, 5], "precis": [1, 3, 6], "possibl": [1, 2, 3, 4, 5, 6], "calc": [1, 2, 3, 6], "keyword": [1, 2, 4, 5], "notic": [1, 2, 3, 4, 5, 6], "finicki": 1, "dot": [1, 6], "underscir": 1, "justif": [1, 2], "format": 1, "indic": [1, 2, 3, 5], "indent": 1, "One": [1, 2, 3, 4, 5, 6], "outlin": [1, 2, 4, 6], "modulo": [1, 4, 5], "individu": 1, "pure": [1, 6], "littl": [1, 2, 6], "underneath": [1, 3], "pow_two": [1, 4, 5], "mul_sub": 1, "add_sub": 1, "sub_sub": 1, "add_zero": [1, 5], "perform": [1, 2, 3], "exact": [1, 2, 3, 4, 5, 6], "becaus": [1, 2, 3, 4, 5, 6], "exactli": [1, 2, 3, 5, 6], "close": [1, 2, 3], "note": [1, 2, 4, 5, 6], "bit": [1, 4, 6], "commut": [1, 2, 3, 4, 5], "indirectli": 1, "data": [1, 2, 4, 5, 6], "similar": [1, 2, 3, 5, 6], "common": [1, 2, 3, 4, 5, 6], "variat": [1, 3, 4, 5, 6], "call": [1, 2, 3, 4, 5, 6], "nth_rewrit": 1, "allow": [1, 2, 3, 4, 5, 6], "particular": [1, 2, 5, 6], "instanc": [1, 2, 3, 4, 5, 6], "enumer": [1, 2], "start": [1, 2, 3, 4, 6, 7, 10], "zero": [1, 2, 3, 4, 5, 6], "occurr": 1, "nth_rw": 1, "nth_rewrite_lh": 1, "nth_rewrite_rh": 1, "sophist": [1, 6], "subexpress": 1, "consist": [1, 3, 5, 6], "collect": [1, 3, 5, 6], "oper": [1, 2, 3, 4, 5, 6], "time": [1, 4, 5, 6], "constant": [1, 2], "mapsto": [1, 5], "abelian": [1, 5], "negat": [1, 5, 10], "invers": [1, 3, 5], "axiom": [1, 3, 5, 6], "add_comm": [1, 4, 5], "zero_add": [1, 4, 5], "add_left_neg": [1, 5], "mul_on": [1, 5], "one_mul": [1, 2, 5], "being": [1, 3, 5, 6], "suffic": [1, 2, 3, 6], "give": [1, 2, 3, 4, 6], "element": [1, 2, 3, 4, 5, 6], "concret": [1, 2, 4, 5, 6], "integ": [1, 2, 4, 10], "abstract": [1, 2, 6, 10], "character": [1, 3, 4, 6], "axiomat": [1, 2, 3, 5], "train": 1, "recogn": [1, 2, 4, 5, 6], "appropri": [1, 2, 3, 5], "\u2124": [1, 4, 5], "ration": [1, 2, 4, 6], "\u211a": [1, 4, 6], "\u2102": [1, 5], "extend": [1, 3, 4, 5, 6], "Not": [1, 5, 6], "properti": [1, 2, 3, 4, 5, 6], "hold": [1, 2, 3, 4, 5, 6], "arbitrari": [1, 2, 3, 4, 5], "taken": [1, 2], "cours": [1, 2, 4, 6], "linear": [1, 2, 5, 6], "matric": [1, 5], "fail": [1, 2, 3, 4, 5, 6], "commr": [1, 2, 5], "unchang": [1, 2], "linarith": [1, 2, 4, 5], "permiss": 1, "strike": [1, 2], "balanc": 1, "concis": [1, 5], "readabl": [1, 2, 3, 4, 6], "strengthen": [1, 2, 4], "skill": [1, 2, 3, 4], "deriv": [1, 2, 4, 7], "most": [1, 2, 3, 4, 5, 6], "content": [1, 4, 6], "organiz": 1, "mechan": [1, 2, 5], "namespac": [1, 2, 3, 4, 5, 6], "shorter": [1, 3, 4, 6], "avoid": [1, 3, 4, 5], "due": [1, 3], "clash": 1, "myre": 1, "add_right_neg": 1, "effect": [1, 3, 6], "temporarili": [1, 2], "reprov": 1, "care": [1, 2, 3, 5], "earlier": 1, "pai": [1, 2, 6], "attent": [1, 2, 4, 6], "curli": [1, 2], "implicit": [1, 2, 5, 6], "moment": [1, 2, 5], "worri": [1, 3, 4, 5], "neg_add_cancel_left": 1, "add_neg_cancel_right": 1, "add_left_cancel": 1, "add_right_cancel": 1, "plan": [1, 6], "brace": 1, "imagin": 1, "situat": [1, 3, 6], "draw": [1, 5], "conclus": [1, 2, 4], "hypothes": [1, 2, 3, 4, 5], "redund": [1, 5, 6], "few": [1, 2, 3, 4, 6], "extra": [1, 2, 3, 5, 6], "oner": 1, "complic": [1, 2], "tediou": [1, 2], "mark": [1, 2, 6], "suppos": [1, 2, 3, 4, 5, 6], "infer": [1, 2, 3, 5], "mul_zero": [1, 5], "serv": [1, 3, 4, 5], "therefor": [1, 4, 5, 6], "promot": 1, "modular": 1, "subproof": 1, "wa": [1, 3], "except": [1, 5], "ad": [1, 2, 3, 4, 5, 6], "free": [1, 6], "At": [1, 2, 4, 5], "rememb": [1, 2, 3, 4, 5, 6], "zero_mul": [1, 2, 4, 5], "By": [1, 3, 5], "neg_eq_of_add_eq_zero": 1, "eq_neg_of_add_eq_zero": 1, "neg_zero": 1, "neg_neg": 1, "had": 1, "annot": [1, 3, 4, 5], "third": [1, 2, 3, 5, 6], "specifi": [1, 2, 3, 4, 5, 6], "imposs": 1, "default": [1, 2, 3, 4, 5], "subtract": [1, 4, 5], "provabl": [1, 3, 6], "sub_eq_add_neg": [1, 5], "On": [1, 2, 3, 5, 6], "defin": [1, 2, 3, 4, 5, 6], "reflex": [1, 2], "present": [1, 2, 4, 6], "forc": [1, 2, 3], "unfold": [1, 2, 3, 4, 5, 6], "refl": [1, 2, 3, 5], "deal": [1, 2, 3, 4, 5, 6], "equat": [1, 2, 3, 4, 5], "interchang": 1, "self_sub": 1, "either": [1, 2, 3, 5, 6], "effort": [1, 4], "one_add_one_eq_two": 1, "norm_num": [1, 2, 4, 5], "strength": 1, "weaker": [1, 2], "notion": [1, 2, 3, 4, 5, 6, 7], "addgroup": 1, "otherwis": [1, 2, 3, 4, 5], "variant": [1, 2, 6], "addcommgroup": 1, "commgroup": 1, "mul_left_inv": [1, 5], "\u00b9": [1, 3, 5, 6], "feel": [1, 2, 6], "cocki": 1, "helper": 1, "along": [1, 4, 6], "hint": [1, 2], "mul_right_inv": [1, 5], "mul_inv_rev": 1, "non": [1, 3, 6], "abel": 1, "noncomm_r": 1, "seem": [1, 2, 4, 6], "odd": [1, 2, 3, 4], "partli": 1, "histor": 1, "conveni": [1, 2, 3, 5, 6], "great": [1, 5], "sort": [1, 3, 4], "inequ": [1, 2, 6], "le": [1, 5], "whenev": [1, 2, 4, 5], "consid": [1, 2, 3, 4, 5, 6, 7], "le_refl": [1, 2], "le_tran": [1, 2, 5], "detail": [1, 2, 3, 4, 5], "unless": [1, 2, 5], "realli": [1, 2, 3, 4, 6], "insist": 1, "discuss": [1, 2, 4, 5, 6], "implic": [1, 6, 10], "h\u2080": [1, 2, 3, 4, 6], "creat": 1, "option": [1, 2, 4, 5, 6], "visibl": 1, "must": [1, 5, 6], "complet": [1, 2, 3, 4], "decreas": [1, 5], "fourth": [1, 2], "mode": [1, 2, 5], "entir": [1, 3, 5, 6], "lt_of_le_of_lt": [1, 2, 5], "lt_of_lt_of_l": 1, "lt_tran": [1, 2], "togeth": [1, 2, 3, 4, 5, 6], "handl": [1, 3, 4], "arithmet": 1, "5": [1, 2, 5, 6], "pass": [1, 5], "exp_le_exp": 1, "mpr": [1, 2, 5, 6], "exp": [1, 3], "applic": [1, 2, 4, 5], "function": [1, 2, 4, 5, 7, 10], "compound": [1, 2, 6], "pars": [1, 3], "exp_lt_exp": 1, "log_le_log": 1, "log": [1, 3], "log_lt_log": 1, "add_le_add": [1, 2, 5], "add_le_add_left": 1, "add_le_add_right": 1, "add_lt_add_of_le_of_lt": 1, "add_lt_add_of_lt_of_l": 1, "add_lt_add_left": 1, "add_lt_add_right": 1, "add_nonneg": [1, 5], "add_po": 1, "add_pos_of_pos_of_nonneg": 1, "exp_po": [1, 3], "bi": [1, 5, 10], "lr": 1, "iff": [1, 3, 6], "connect": [1, 3, 5, 6], "equival": [1, 2, 3, 4, 5, 6], "mp": [1, 2, 3, 4, 6], "forward": [1, 2, 5, 6], "direct": [1, 2, 3, 6], "stand": [1, 2, 5, 6], "modu": 1, "ponen": 1, "respect": [1, 2, 3, 4, 5, 6], "thu": [1, 3, 4, 5, 6], "again": [1, 2, 3, 4, 5, 6], "numer": [1, 4, 5], "constitut": 1, "part": [1, 2, 3, 4, 5, 6], "strategi": [1, 2, 4], "api": 1, "reli": [1, 2, 3, 5, 6], "guess": [1, 2, 3, 4, 5], "a_of_b_of_c": 1, "approxim": 1, "loud": 1, "probabl": [1, 5, 6], "add_l": 1, "choic": [1, 2, 3, 5, 6], "exist": [1, 2, 3, 6], "jump": [1, 4, 5, 6], "nearbi": [1, 4], "library_search": [1, 4], "sq_nonneg": 1, "delet": [1, 2, 3, 4], "uncom": 1, "previou": [1, 2, 3, 5, 6], "suggest": [1, 2, 4, 5, 6], "long": [1, 2, 3, 5], "better": [1, 3, 4, 5, 6], "confirm": [1, 2, 3, 4], "finish": [1, 2, 3, 4], "job": 1, "pow_two_nonneg": [1, 2], "tend": [1, 6], "around": [1, 3, 6], "binari": [1, 2, 4, 5], "increas": 1, "worth": [1, 2, 5], "definition": [1, 4, 5, 6], "principl": [1, 2, 3, 4], "favor": [1, 2, 5], "timesav": 1, "clever": 1, "involv": [1, 2, 4, 5, 6], "nice": [1, 2, 4, 6], "idea": [1, 2, 3, 5, 6], "abs_l": [1, 5], "ab": [1, 2, 5], "congratul": [1, 2, 4], "becom": [1, 4, 5, 6], "min": [1, 2, 6], "uniqu": [1, 2, 3, 4, 5, 6], "min_le_left": 1, "min_le_right": 1, "le_min": 1, "max": [1, 2, 6], "pair": [1, 2, 4, 5, 6], "act": 1, "curri": 1, "logician": 1, "haskel": 1, "get": [1, 2, 3, 4, 6, 10], "bind": [1, 3], "tighter": [1, 3], "infix": 1, "le_antisymm": [1, 2], "less": [1, 2, 3, 4, 5, 6], "usag": 1, "inconsist": 1, "outer": 1, "level": [1, 2], "nest": [1, 2], "maintain": 1, "bother": [1, 3], "repetit": 1, "foreshadow": 1, "univers": [1, 3, 5, 6, 10], "quantifi": [1, 3, 4, 5, 6, 10], "desir": [1, 3, 6], "implicitli": [1, 2], "mani": [1, 2, 3, 5, 6, 10], "whether": [1, 2, 3, 4, 6], "Of": [1, 2, 4, 6], "interest": [1, 2, 3, 5, 6], "vice": [1, 3], "versa": [1, 3], "word": [1, 2, 3, 4, 5, 6], "switch": 1, "transit": [1, 2, 5, 6], "total": 1, "satisfi": [1, 3, 4, 5, 6], "disjunct": [1, 3, 10], "stick": [1, 2, 6, 7], "split": [1, 2, 3, 4], "aux": [1, 2, 4, 6], "valu": [1, 2, 3, 4, 5, 6], "yield": [1, 2, 3, 4, 5, 6], "made": [1, 2, 3, 5, 6], "manifest": [1, 6], "triangl": [1, 2, 5], "abs_add": [1, 2], "sub_add_cancel": [1, 5], "relat": [1, 2, 3, 5, 6], "ordinari": [1, 2, 4, 5, 6], "unicod": [1, 3], "obtain": [1, 2, 4, 5, 6], "dvd": 1, "dvd_tran": 1, "dvd_mul_of_dvd_left": 1, "dvd_mul_left": 1, "expon": 1, "expand": [1, 2, 3, 4, 5], "w": 1, "greatest": [1, 5, 6], "divisor": [1, 2, 4, 5], "gcd": [1, 2, 4], "least": [1, 5, 6], "lcm": 1, "analog": [1, 2, 3, 4, 5, 6], "divid": [1, 2, 4, 5], "gcd_zero_right": 1, "gcd_zero_left": 1, "lcm_zero_right": 1, "lcm_zero_left": 1, "similarli": [1, 2, 3, 4, 5], "prefix": [1, 4], "dvd_antisymm": 1, "complain": 1, "ambigu": [1, 5], "_root_": 1, "saw": [1, 5, 6], "govern": [1, 5], "class": [1, 4, 5, 6, 7], "describ": [1, 2, 3, 4, 5, 6], "\u03b1": [1, 2, 3, 4, 5, 6], "partialord": [1, 2], "adopt": 1, "letter": [1, 5], "\u03b2": [1, 2, 3, 5, 6], "\u03b3": [1, 2, 5, 6], "greek": [1, 4], "especi": [1, 5, 6], "strict": [1, 2], "somewhat": [1, 3, 6], "lt_irrefl": [1, 2], "lt_iff_le_and_n": 1, "lattic": [1, 5, 6], "inf_le_left": [1, 6], "inf_le_right": 1, "le_inf": 1, "le_sup_left": 1, "le_sup_right": 1, "sup_l": 1, "lower": [1, 2, 4], "bound": [1, 2, 3, 4, 5, 6], "upper": [1, 2], "glb": 1, "lub": 1, "infimum": [1, 6], "supremum": [1, 4], "inf": [1, 6], "sup": [1, 4, 6], "further": [1, 6], "matter": [1, 2], "meet": [1, 2, 3, 5], "join": [1, 5], "keep": [1, 5], "dictionari": 1, "subset": [1, 2, 3, 5, 6], "domain": [1, 2, 3, 4, 5, 6], "boolean": 1, "truth": [1, 4], "fals": [1, 2, 3, 4], "true": [1, 2, 3, 6], "posit": [1, 3, 4, 5, 6], "subspac": 1, "vector": [1, 3], "intersect": [1, 3, 5, 6], "sum": [1, 2, 4, 5, 6], "inclus": [1, 3, 6], "topolog": [1, 5, 10], "union": [1, 3, 4, 5], "inf_comm": 1, "inf_assoc": 1, "sup_comm": 1, "sup_assoc": 1, "absorpt": 1, "law": 1, "absorb1": 1, "absorb2": 1, "found": [1, 5], "inf_sup_self": 1, "sup_inf_self": 1, "distriblattic": 1, "inf_sup_left": 1, "inf_sup_right": 1, "sup_inf_left": 1, "sup_inf_right": 1, "shown": [1, 5], "explicit": [1, 2, 5, 6], "nondistribut": 1, "finit": [1, 3, 4, 5, 6], "impli": [1, 2, 3, 4, 5, 6], "larger": [1, 6], "carrier": [1, 5], "compat": [1, 6], "strictorderedr": 1, "mul_po": [1, 4], "mul_nonneg": 1, "coupl": [1, 2, 6], "metric": [1, 5, 10], "equip": [1, 3, 5, 6], "distanc": [1, 2, 6], "dist": [1, 6], "map": [1, 2, 3, 5, 6], "metricspac": [1, 6], "dist_self": 1, "dist_comm": [1, 6], "dist_triangl": [1, 6], "nonneg": [1, 5], "nonneg_of_mul_nonneg_left": 1, "dist_nonneg": [1, 6], "dealt": 2, "basic": [2, 4, 5, 6, 10], "simpl": [2, 4, 5], "absolut": 2, "\u03b5": [2, 6], "though": [2, 3, 4, 5], "treat": [2, 3, 5, 6], "my_lemma": 2, "\u03b4": [2, 6], "hb": [2, 6], "subsequ": [2, 4, 6], "lemma": [2, 4, 5, 6, 10], "my_lemma2": 2, "stage": [2, 5], "my_lemma3": 2, "epo": 2, "ele1": 2, "xlt": 2, "ylt": 2, "essenti": [2, 3, 5, 6], "colon": 2, "why": [2, 4, 6], "off": [2, 3, 4], "my_lemma4": 2, "abs_mul": 2, "mul_le_mul": 2, "abs_nonneg": 2, "mul_lt_mul_right": 2, "extract": [2, 6], "hidden": 2, "expos": [2, 6], "predic": [2, 3, 4, 6], "fn_ub": 2, "fn_lb": 2, "fnub": 2, "fnlb": 2, "hfa": 2, "hgb": 2, "dsimp": [2, 3, 4, 5], "simplif": [2, 3, 4], "contract": 2, "anyhow": 2, "control": 2, "transform": [2, 3], "rest": [2, 3, 5, 6], "routin": 2, "nnf": 2, "nng": 2, "hfb": 2, "nna": 2, "order": [2, 3, 4, 5, 6, 10], "codomain": [2, 4, 6], "structur": [2, 4, 6, 10], "monoid": [2, 3, 4], "fn_ub_add": 2, "orderedcanceladdcommmonoid": 2, "high": 2, "monoton": [2, 6], "nondecreas": [2, 4], "placehold": 2, "Or": [2, 3], "backward": [2, 6], "subgoal": 2, "mf": 2, "mg": 2, "aleb": 2, "lambda": [2, 5], "underscor": [2, 3], "flag": [2, 3], "squiggli": 2, "marker": 2, "nnc": 2, "bbb": [2, 5], "fneven": 2, "fnodd": 2, "ef": 2, "eg": 2, "og": 2, "shorten": 2, "rid": 2, "won": [2, 4, 6], "cannot": [2, 3, 4, 5, 6], "contrari": 2, "syntact": 2, "reduct": [2, 3], "erw": 2, "harder": 2, "spot": 2, "rudimentari": 2, "foundat": [2, 3, 4, 5], "impos": 2, "restrict": [2, 3, 4, 6], "talk": [2, 4, 6], "assert": [2, 3], "ask": [2, 4, 5, 6], "xs": [2, 3], "tran": [2, 4, 5], "setub": 2, "inject": [2, 3, 4, 6], "x_1": [2, 3], "x_2": [2, 3], "x\u2081": [2, 3, 5, 6], "x\u2082": [2, 3, 5], "add": [2, 4, 5, 6], "nonzero": [2, 4, 5], "add_left_inj": 2, "composit": [2, 3, 5, 6], "injg": 2, "injf": [2, 3], "canon": [2, 3, 4, 5], "exhibit": [2, 6], "anonym": [2, 3, 4, 5], "constructor": [2, 3, 4, 5], "angl": 2, "whatev": [2, 4], "certain": [2, 6], "fnhasub": 2, "fnhaslb": 2, "fnub_add": 2, "gun": 2, "ubf": 2, "ubg": 2, "ubfa": 2, "ubfb": 2, "unpack": [2, 3], "claus": 2, "whose": [2, 4, 5, 6], "els": [2, 3, 4], "turn": [2, 3, 4, 5, 6, 7], "directli": [2, 4, 5, 6], "lbf": 2, "lbg": 2, "cousin": 2, "rcase": [2, 3, 4, 5, 6], "flexibl": [2, 6], "recurs": [2, 3, 5, 10], "harm": [2, 3], "swiss": 2, "armi": 2, "knive": 2, "wide": 2, "old": [2, 5], "chestnut": 2, "product": [2, 4, 5, 6], "magic": [2, 5], "verifi": 2, "sumofsquar": 2, "sumofsquares_mul": 2, "sosx": 2, "sosi": 2, "xeq": [2, 3], "yeq": 2, "insight": 2, "motiv": 2, "gaussian": [2, 10], "i": [2, 3, 4, 5, 6], "sqrt": [2, 3, 4, 5], "norm": [2, 5, 6], "reflect": 2, "di": [2, 5], "xy": [2, 5], "cryptic": 2, "easiest": [2, 4], "perspicu": 2, "divis": [2, 4, 5, 10], "divab": 2, "divbc": 2, "beq": 2, "ceq": 2, "And": [2, 4, 6], "pretti": [2, 6], "Then": [2, 3, 5, 6], "divac": 2, "alpha": [2, 3], "beta": [2, 3], "surject": [2, 3, 6], "yourself": [2, 5], "field_simp": [2, 5], "denomin": [2, 4, 5], "div_mul_cancel": 2, "hx": [2, 3, 5], "method": [2, 3, 4, 5], "surjg": 2, "surjf": [2, 3], "strictli": 2, "contradict": [2, 3, 4], "speak": [2, 5, 6], "irreflex": 2, "asymmetri": 2, "lt_asymm": 2, "sugar": 2, "eventu": [2, 3, 6], "fnuba": 2, "not_le_of_gt": 2, "not_lt_of_g": [2, 4, 5], "lt_of_not_g": 2, "le_of_not_gt": 2, "snippet": [2, 4, 5], "counterexampl": 2, "monof": 2, "noth": [2, 3, 4, 5], "four": [2, 5], "valid": 2, "far": [2, 3, 6], "q": [2, 4, 5, 6], "straightforward": 2, "difficult": 2, "conclud": 2, "nonexist": 2, "contradictori": 2, "classic": [2, 3, 4], "by_contra": [2, 4], "not_not": 2, "front": 2, "push": [2, 4, 6], "inward": 2, "facilit": [2, 6], "push_neg": [2, 3, 4], "restat": 2, "contrapos": [2, 3, 4], "yet": [2, 3, 4, 5, 6], "semicolon": [2, 4], "falso": 2, "anyth": [2, 5, 6], "elim": 2, "strang": [2, 4], "fairli": 2, "reach": 2, "37": 2, "exfalso": 2, "absurd": [2, 4], "slick": 2, "drop": 2, "manner": [2, 5], "contrast": [2, 3, 5, 6], "compon": [2, 3, 5, 6], "techniqu": [2, 6], "variou": [2, 3, 5], "xltz": 2, "zlty": 2, "10": 2, "7": [2, 4, 6], "behav": [2, 3, 6], "roughli": [2, 3, 4], "friend": [2, 5], "were": [2, 4, 5, 6], "inscrut": [2, 3], "gadget": [2, 6], "auxiliari": [2, 6], "pow_eq_zero": [2, 4], "doubl": [2, 3], "symmetr": [2, 3], "abs_lt": 2, "dvd_gcd_iff": 2, "8": [2, 4, 6], "6": [2, 4, 5, 6], "15": 2, "below": [2, 3, 4, 5, 6], "not_monotone_iff": 2, "antisymmetr": 2, "aris": 2, "preorder": [2, 6], "pre": 2, "lt_iff_le_not_l": 2, "beyond": 2, "repeatedli": [2, 6], "instanti": [2, 5, 6], "inl": [2, 3], "inr": [2, 3], "produc": 2, "branch": [2, 3], "le_or_gt": 2, "abs_of_nonneg": [2, 5], "abs_of_neg": 2, "immedi": [2, 3, 5], "myab": 2, "le_abs_self": [2, 5], "neg_le_abs_self": 2, "enjoi": [2, 3, 4, 6], "pun": 2, "lt_ab": 2, "genuin": 2, "vertic": [2, 5], "lt_trichotomi": 2, "xgt": 2, "dvd_mul_right": [2, 4], "eq_zero_or_eq_zero_of_mul_eq_zero": 2, "nontrivi": [2, 3, 4, 5, 6], "integr": [2, 7], "isdomain": 2, "em": [2, 3], "exclud": [2, 4], "by_cas": [2, 3, 4], "dispos": 2, "s_0": [2, 3], "s_1": 2, "s_2": 2, "ldot": [2, 3, 4], "varepsilon": [2, 6], "s_n": [2, 3], "render": [2, 4], "convergesto": 2, "ext": [2, 3, 4, 5], "enabl": [2, 3, 4, 5], "actual": [2, 3, 4, 6], "u": [2, 3, 5, 6], "v": [2, 3, 5, 6], "congr": 2, "reconcil": 2, "peel": 2, "convert": [2, 4], "quit": [2, 6], "zero_lt_on": [2, 4], "fill": [2, 3, 4, 5], "convergesto_const": 2, "\u03b5po": [2, 6], "nge": 2, "abs_zero": 2, "save": [2, 3], "troubl": [2, 3, 5], "pen": 2, "paper": [2, 3, 5, 6], "ns": 2, "nt": 2, "maximum": [2, 4, 6], "implement": [2, 5], "convergesto_add": 2, "cs": 2, "ct": 2, "\u03b52po": 2, "hs": [2, 4, 6], "ht": 2, "le_of_max_le_left": 2, "le_of_max_le_right": 2, "tricki": [2, 3, 4], "convergesto_mul_const": 2, "mulzeroclass": 2, "acpo": 2, "abs_po": 2, "independ": [2, 3, 5], "exists_abs_le_of_convergesto": 2, "strong": [2, 4], "n\u2080": 2, "bpo": [2, 6], "pos\u2080": 2, "div_po": 2, "n\u2081": 2, "convergesto_mul": 2, "sketch": [2, 3, 4, 6], "limit": [2, 6], "bold": 2, "scratch": 2, "convergesto_uniqu": 2, "sa": 2, "sb": 2, "abn": 2, "na": 2, "hna": 2, "nb": 2, "hnb": 2, "absa": 2, "absb": 2, "observ": [2, 4, 6], "everywher": [2, 3, 6], "linearord": 2, "vastli": 2, "awai": [2, 5], "vocabulari": 3, "uniform": [3, 6], "primit": 3, "conceptu": 3, "advantag": [3, 4, 5], "overload": 3, "verbos": 3, "system": [3, 4, 5], "wrong": 3, "theoret": [3, 6], "ss": 3, "sub": [3, 6], "cap": 3, "un": 3, "cup": 3, "univ": [3, 6], "empti": [3, 4, 5, 6], "member": [3, 6], "membership": [3, 4], "mem": 3, "notin": 3, "ident": [3, 4, 5, 6, 10], "databas": [3, 4, 6], "unlik": [3, 4], "existenti": [3, 10], "subset_def": 3, "inter_def": 3, "xu": 3, "mem_inter_iff": 3, "xsu": 3, "phenomenon": 3, "quirk": 3, "pitfal": 3, "heavili": [3, 6], "fall": 3, "union_def": 3, "mem_union": [3, 4], "xtu": 3, "xt": 3, "unnecessari": 3, "clearer": [3, 5], "correctli": 3, "special": [3, 4, 5, 6], "rewritten": 3, "diff_eq": 3, "mem_diff": 3, "xstu": 3, "xnt": 3, "xnu": 3, "extension": [3, 5], "unsurprisingli": 3, "dollar": 3, "sign": [3, 6], "and_comm": 3, "antisymm": 3, "hood": [3, 5], "builder": 3, "trivial": [3, 4, 6], "eq_two_or_odd": 3, "even_iff": 3, "confus": [3, 4, 6], "fortun": 3, "agre": 3, "prime_iff": 3, "symm": [3, 4, 5, 6], "rwa": [3, 4, 5], "signific": 3, "ball": 3, "bex": 3, "bex_def": 3, "prime_x": 3, "slight": 3, "ssubt": 3, "index": [3, 6], "model": [3, 6], "sequenc": [3, 6, 10], "a_0": 3, "a_1": 3, "a_2": 3, "mem_iunion": 3, "xai": 3, "mem_iint": 3, "mem_union\u2082": 3, "mem_inter\u2082": 3, "mem_iunion\u2082": 3, "exists_prime_and_dvd": 3, "eq_univ": 3, "eq_univ_of_foral": 3, "exists_infinite_prim": 3, "\u2080": 3, "sunion": 3, "sinter": 3, "relationship": [3, 4], "mem_iinter\u2082": 3, "sunion_eq_biunion": 3, "sinter_eq_biint": 3, "preimag": [3, 6], "imag": [3, 4, 6], "tripl": 3, "tag": 3, "mem_image_of_mem": 3, "galoi": [3, 5, 6], "image_subset_iff": 3, "represent": [3, 4, 5], "asid": 3, "raini": 3, "dai": 3, "behavior": [3, 6], "nonempti": [3, 6], "condit": [3, 4, 6], "fxeq": 3, "ai": 3, "fx": 3, "eq": [3, 5], "injon": 3, "theme": 3, "rel": [3, 5], "relativ": 3, "xpo": 3, "ypo": 3, "exp_log": 3, "ingredi": [3, 5, 6], "assign": [3, 5], "inhabit": [3, 5, 6], "appeal": 3, "choose_spec": 3, "some_spec": 3, "noncomput": [3, 5], "inverse_spec": 3, "dif_po": 3, "dif_neg": 3, "fulli": [3, 6], "alon": 3, "leftinvers": 3, "rightinvers": 3, "hack": 3, "half": 3, "dozen": 3, "condens": 3, "cantor": 3, "famou": 3, "miss": [3, 4], "j": [3, 5], "intuit": [3, 6], "cardin": 3, "biject": [3, 5], "nineteenth": 3, "centuri": 3, "infinit": [3, 6, 10], "dedekind": 3, "quickli": 3, "behind": 3, "problem": [3, 4, 5, 6], "shade": 3, "region": 3, "diagram": 3, "circ": [3, 5], "scale": 3, "inner": 3, "smaller": [3, 4, 6], "concentr": 3, "unshad": 3, "compos": [3, 5, 6], "disjoint": 3, "sound": [3, 5], "plausibl": 3, "delic": 3, "improv": [3, 4], "confid": 3, "invfun": [3, 5], "leftinverse_invfun": 3, "invfun_eq": 3, "sbaux": 3, "sbset": 3, "sb_aux": 3, "s_": 3, "sb_set": 3, "bigcup_": 3, "mathbb": [3, 4, 5], "sbfun": 3, "complement": [3, 6], "outermost": 3, "setminu": 3, "inv_fun": 3, "inv_fun_eq": 3, "sb_right_inv": 3, "goe": [3, 4, 5, 6], "henc": [3, 4, 5, 6], "neither": [3, 5], "nor": [3, 5], "sb_inject": 3, "hf": [3, 6], "hg": [3, 6], "a_def": 3, "h_def": 3, "hxeq": 3, "xa": [3, 5], "wlog": 3, "x\u2081a": 3, "resolve_left": 3, "x\u2082a": 3, "not_imp_self": 3, "x\u2082na": 3, "if_po": 3, "if_neg": 3, "x\u2082eq": 3, "hn": [3, 4, 6], "sb_fun": 3, "bring": [3, 4, 6], "tradeoff": 3, "encapsul": [3, 5], "symmetri": 3, "dwell": 3, "succ": [3, 4], "sb_surject": 3, "gya": 3, "xmem": 3, "sweet": 3, "schroeder_bernstein": 3, "substant": 4, "ancient": 4, "fraction": 4, "lowest": 4, "2c": 4, "4c": 4, "factor": [4, 5], "coprim": 4, "smart": 4, "12": 4, "encount": 4, "algebra": [4, 6, 10], "prime_def_lt": 4, "eq_one_or_self_of_dvd": 4, "prime_p": 4, "17": 4, "commonli": [4, 5], "prime_two": 4, "prime_thre": 4, "broader": [4, 7], "irreduc": [4, 5], "coincid": [4, 5, 6], "rise": 4, "dvd_mul": 4, "even_of_even_sqr": 4, "dvd_of_dvd_pow": 4, "proce": 4, "profici": 4, "ctrl": [4, 5], "search": [4, 5], "engin": 4, "hesit": 4, "mul_right_inj": 4, "heart": 4, "irration": 4, "dvd_gcd": 4, "coprime_mn": 4, "sqr_eq": 4, "meq": 4, "dvd_iff_exists_eq_mul_left": 4, "two_l": 4, "le_of_dvd": 4, "approach": [4, 5, 6], "quick": 4, "ne": [4, 5], "occur": 4, "suffici": [4, 6], "permut": 4, "prime_of_mem_factor": 4, "prod_factor": 4, "factors_uniqu": 4, "factorization_mul": 4, "mnez": 4, "nnez": 4, "factorization_pow": 4, "black": 4, "box": 4, "simpa": 4, "nnz": 4, "nsqr_nez": 4, "eq1": 4, "eq2": 4, "add_mul_mod_self_left": 4, "mul_mod_right": 4, "count_factors_mul_of_po": 4, "successor": 4, "succ_ne_zero": 4, "npow_nz": 4, "dvd_sub": 4, "pow_eq": 4, "npowz": 4, "add_sub_cancel": 4, "understood": [4, 6], "quotient": [4, 5, 6], "pictur": [4, 5], "mediat": 4, "headach": 4, "contend": 4, "issu": [4, 5, 6], "th": 4, "topic": 4, "enat": 4, "infin": [4, 6], "appreci": 4, "role": [4, 5, 6], "_section_induction_and_recurs": 4, "writ": 4, "datatyp": 4, "freeli": 4, "translat": [4, 6], "mathematician": [4, 6], "inj": 4, "factori": 4, "fac": 4, "ih": 4, "fac_po": 4, "succ_po": 4, "dvd_fac": 4, "ipo": 4, "il": 4, "of_le_succ": 4, "dvd_mul_of_dvd_right": 4, "crude": 4, "remaind": [4, 5], "pow_two_le_fac": 4, "finset": [4, 5, 6], "bigoper": [4, 5], "prod": [4, 6], "sum_range_zero": 4, "sum_range_succ": 4, "summat": 4, "prod_range_zero": 4, "prod_range_succ": 4, "deserv": 4, "comment": 4, "danger": [4, 5], "ordinarili": [4, 5], "loop": 4, "indefinit": 4, "fix": [4, 6], "placement": 4, "re": [4, 5], "handi": 4, "sum_id": 4, "div_eq_of_eq_mul_right": 4, "succ_eq_add_on": 4, "sum_sqr": 4, "mynat": 4, "thumb": 4, "decid": [4, 6], "preced": 4, "truncat": 4, "exponenti": 4, "cut": 4, "predecessor": 4, "pred": 4, "mul": [4, 5, 6], "succ_add": 4, "succ_mul": 4, "explor": [4, 6], "standard": [4, 5, 6], "formul": [4, 6], "quirki": 4, "among": 4, "annoi": 4, "h0": 4, "succ_le_succ": 4, "zero_l": [4, 5], "interval_cas": 4, "interv": [4, 6], "decis": 4, "procedur": 4, "revert": [4, 5], "minfac": 4, "smallest": [4, 6], "strong_induction_on": 4, "subsum": 4, "exists_prime_factor": 4, "np": 4, "mltn": 4, "mdvdn": 4, "mne1": 4, "mz": 4, "zero_dvd_iff": 4, "mgt2": 4, "pp": 4, "pdvd": 4, "factorial_po": 4, "dvd_factori": 4, "primes_infinit": 4, "refin": 4, "ple": 4, "p_1": 4, "p_n": 4, "prod_": 4, "p_i": [4, 6], "computation": 4, "test": 4, "decidableeq": 4, "abandon": 4, "ourselv": 4, "subset_iff": 4, "mem_int": 4, "mem_sdiff": 4, "tauto": 4, "dispens": 4, "tautolog": 4, "dvd_prod_of_mem": 4, "eq_of_dvd_of_prim": 4, "prime_q": 4, "preserv": [4, 6], "induction_on": 4, "singleton": 4, "prod_empti": 4, "prod_insert": 4, "mem_of_dvd_prod_prim": 4, "mem_insert": 4, "wrote": 4, "filter": [4, 10], "mem_filt": 4, "aim": 4, "prod_po": 4, "_def": 4, "mem_": 4, "id": [4, 6], "bounded_of_ex_finset": 4, "qk": 4, "lt_succ_of_l": 4, "le_sup": 4, "ex_finset_of_bound": 4, "decidablepr": 4, "lt_succ_iff": 4, "congruent": 4, "p_k": 4, "loss": 4, "27": 4, "mod_4_eq_3_or_mod_4_eq_3": 4, "mul_mod": 4, "mod_lt": 4, "hm": 4, "two_le_of_mod_4_eq_3": 4, "neq": 4, "div_dvd_of_dvd": 4, "div_lt_self": 4, "piec": [4, 5, 6], "exists_prime_factor_mod_4_eq_3": 4, "dvd_rfl": 4, "mge2": 4, "mul_div_cancel": 4, "home": [4, 5], "stretch": [4, 5], "remov": [4, 6], "eras": 4, "mem_eras": 4, "readi": [4, 6], "dvd_add_iff_left": 4, "primes_mod_4_eq_3_infinit": 4, "p4": 4, "pltn": 4, "p4eq": 4, "ps": 4, "pne3": 4, "seriou": [4, 6], "feat": 4, "modern": 5, "subject": 5, "mysteri": 5, "technic": 5, "consult": 5, "ann": 5, "baanen": 5, "abus": 5, "paramet": 5, "broadest": 5, "constraint": [5, 6], "bundl": [5, 6], "tupl": 5, "hy": 5, "hz": 5, "mypoint1": 5, "mypoint2": 5, "mypoint3": 5, "mk": [5, 6], "former": 5, "latter": [5, 6], "quot": [5, 6], "protect": 5, "intern": 5, "add_x": 5, "addalt": 5, "etc": [5, 6], "y\u2081": 5, "z\u2081": 5, "y\u2082": 5, "z\u2082": 5, "addalt_x": 5, "addalt_comm": 5, "ya": 5, "za": 5, "xb": 5, "yb": 5, "zb": 5, "apart": 5, "effici": [5, 6], "scalar": 5, "smul": 5, "smul_distrib": 5, "road": 5, "link": 5, "belong": [5, 6], "simplex": 5, "convinc": 5, "equilater": 5, "interior": 5, "standardtwosimplex": 5, "x_nonneg": 5, "y_nonneg": 5, "z_nonneg": 5, "sum_eq": 5, "swap": 5, "swapxi": 5, "interestingli": 5, "midpoint": 5, "div_nonneg": 5, "weight": 5, "averag": 5, "weightedaverag": 5, "lambda_nonneg": 5, "lambda_l": 5, "fin": 5, "standardsimplex": 5, "sum_eq_on": 5, "div_eq_mul_inv": 5, "sum_mul": 5, "sum_add_distrib": 5, "mul_sum": 5, "manipul": [5, 6], "islinear": 5, "is_addit": 5, "preserves_mul": 5, "linf": 5, "subtyp": [5, 6], "preal": 5, "val": 5, "sigma": 5, "wherebi": [5, 6], "stdsimplex": 5, "\u03c3": 5, "fst": [5, 6], "snd": [5, 6], "custom": 5, "robust": 5, "interfac": 5, "redefin": 5, "accessor": 5, "weav": 5, "rich": 5, "interconnect": 5, "hierarchi": 5, "clarifi": 5, "antireflex": 5, "cdot": 5, "mathcal": 5, "proxi": 5, "bipartit": 5, "graph": 5, "categori": [5, 6], "morphism": 5, "basi": [5, 6], "discret": 5, "inherit": 5, "polynomi": 5, "coeffici": 5, "dual": [5, 6], "accommod": 5, "almost": [5, 6], "marriag": 5, "heaven": 5, "group\u2081": 5, "inv": 5, "struc": 5, "counterpart": 5, "chosen": 5, "assur": 5, "groupcat": 5, "group\u2081cat": 5, "str": 5, "capit": 5, "roman": 5, "equiv": 5, "tofun": 5, "right_inv": 5, "left_inv": 5, "creativ": 5, "evid": 5, "coercion": [5, 6], "omit": 5, "perm": 5, "under": [5, 6], "orient": 5, "permgroup": 5, "trans_assoc": 5, "trans_refl": 5, "refl_tran": 5, "self_trans_symm": 5, "grouptheori": 5, "g_1": 5, "g_2": 5, "g_3": 5, "tightli": 5, "isomorph": 5, "additivegroup": 5, "Its": 5, "neg": [5, 6], "reproduc": 5, "accompani": 5, "addgroup\u2081": 5, "scheme": 5, "add_group_point": 5, "add_group\u2081": 5, "arrang": 5, "mul_inv_cancel_right": 5, "achiev": [5, 6], "silent": 5, "regist": 5, "grp": 5, "contextu": 5, "cue": 5, "synthes": 5, "whole": 5, "_inst_1": 5, "candid": 5, "group\u2082": 5, "mysquar": 5, "my_squar": 5, "remark": 5, "head": 5, "store": 5, "headi": 5, "hasmulgroup\u2082": 5, "hasonegroup\u2082": 5, "hasinvgroup\u2082": 5, "suppli": 5, "accord": 5, "capabl": 5, "chain": 5, "recent": 5, "prioriti": 5, "bad": [5, 6], "artifici": 5, "addgroup\u2082": 5, "subtl": [5, 6], "configur": 5, "invis": 5, "wise": 5, "euclidean": 5, "terminolog": 5, "mid": 5, "imaginari": 5, "gaussint": 5, "im": 5, "pointwis": [5, 6], "root": [5, 10], "ac": 5, "bci": 5, "adi": 5, "bd": 5, "bc": 5, "hasmul": 5, "zero_def": 5, "one_def": 5, "add_def": 5, "neg_def": 5, "mul_def": 5, "zero_r": 5, "zero_im": 5, "one_r": 5, "one_im": 5, "add_r": 5, "add_im": 5, "neg_r": 5, "neg_im": 5, "mul_r": 5, "mul_im": 5, "surprisingli": 5, "concept": [5, 6], "light": 5, "bulb": 5, "skeleton": [5, 6], "scari": 5, "entri": 5, "instcommr": 5, "left_distrib": 5, "right_distrib": 5, "ext_iff": 5, "bq": 5, "archetyp": 5, "int": 5, "ediv_add_emod": 5, "emod_nonneg": 5, "emod_lt": 5, "unit": [5, 6], "algorithm": 5, "conjug": 5, "frac": 5, "nearest": 5, "size": 5, "vi": 5, "multipli": 5, "view": [5, 6], "emb": 5, "forth": 5, "quadrat": 5, "gaussian_int": 5, "stai": 5, "face": [5, 6], "machineri": [5, 6], "adapt": 5, "invest": 5, "pragmat": 5, "seek": 5, "heather": 5, "macbeth": 5, "eleg": 5, "div": 5, "mod": 5, "_add_mod": 5, "abs_mod": 5, "_le": 5, "emod_lt_of_po": 5, "zero_lt_two": 5, "fixm": 5, "_eq": 5, "sq_add_sq_eq_zero": 5, "linearorderedr": 5, "norm_nonneg": 5, "norm_eq_zero": 5, "norm_po": 5, "norm_mul": 5, "conj": 5, "conj_r": 5, "conj_im": 5, "norm_conj": 5, "bespok": 5, "quad": 5, "record": 5, "div_def": 5, "mod_def": 5, "messi": 5, "nicer": [5, 6], "norm_mod_lt": 5, "norm_y_po": 5, "sub_mul": 5, "conv": 5, "lh": 5, "sq_le_sq": 5, "mul_le_mul_of_nonneg_left": 5, "ediv_mul_l": 5, "ediv_nonneg": 5, "le_of_mul_le_mul_right": 5, "ediv_lt_of_lt_mul": 5, "natab": 5, "coe_natabs_norm": 5, "natabs_of_nonneg": 5, "natabs_norm_mod_lt": 5, "ofnat_lt": 5, "coe_natab": 5, "not_norm_mul_left_lt_norm": 5, "natabs_mul": 5, "le_mul_of_one_le_right": 5, "ofnat_l": 5, "add_one_le_of_lt": 5, "euclideandomain": 5, "quotient_mul_add_remainder_eq": 5, "quotient_zero": 5, "r_wellfound": 5, "remainder_lt": 5, "mul_left_not_lt": 5, "payoff": 5, "principalidealr": 5, "irreducible_iff_prim": 5, "calculu": 6, "quantiti": 6, "studi": 6, "begun": 6, "paradox": 6, "layer": 6, "naiv": 6, "slightli": 6, "exot": 6, "intermedi": 6, "x\u2080": 6, "convention": 6, "eight": 6, "varieti": 6, "wish": 6, "64": 6, "y\u2080": 6, "z\u2080": 6, "paragraph": 6, "512": 6, "bourbaki": 6, "spell": 6, "dualli": 6, "arbitrarili": 6, "neighborhood": 6, "at_top": 6, "\ud835\udcdd": 6, "\ud835\udce4": 6, "entourag": 6, "\u03bc": 6, "a_": 6, "univ_set": 6, "sets_of_superset": 6, "inter_set": 6, "blur": 6, "princip": 6, "\ud835\udcdf": 6, "demonstr": 6, "opportun": 6, "x_0": 6, "ioo": 6, "tendsto\u2081": 6, "tendsto": 6, "lim_": 6, "sourc": 6, "abstractli": 6, "hide": 6, "salient": 6, "pushforward": 6, "f_": 6, "ve": 6, "tendsto\u2082": 6, "via": 6, "promis": 6, "leverag": 6, "map_mono": 6, "map_map": 6, "shot": 6, "256": 6, "pullback": 6, "comap": 6, "map_le_iff_le_comap": 6, "contravari": 6, "comap_comap": 6, "shift": 6, "plane": 6, "\u1da0": 6, "nhds_prod_eq": 6, "aforement": 6, "le_inf_iff": 6, "attop": 6, "bottom": 6, "shouldn": 6, "prohibit": 6, "global": 6, "precondit": 6, "closur": 6, "ne_bot": 6, "tour": 6, "claim": 6, "recaptur": 6, "superfici": 6, "stronger": 6, "famili": 6, "\u03b9": 6, "select": 6, "hasbasi": 6, "nhds_basis_ioo_po": 6, "has_basi": 6, "tendsto_iff": 6, "reformul": 6, "ici": 6, "attop_basi": 6, "knew": 6, "gave": 6, "n_p": 6, "n_q": 6, "tiresom": 6, "unpleas": 6, "superscript": 6, "hp": 6, "hq": 6, "eventually_eq": 6, "tendsto_congr": 6, "review": 6, "ensur": 6, "eventually_of_foral": 6, "mono": 6, "item": 6, "filter_upward": 6, "hr": 6, "reader": 6, "ae": 6, "aka": 6, "occasion": 6, "frequent": 6, "mem_closure_of_tendsto": 6, "cluster_pt": 6, "mem_closure_iff_clusterpt": 6, "le_principal_iff": 6, "nebot_of_l": 6, "hux": 6, "hum": 6, "dist_eq_zero": 6, "emetricspac": 6, "pseudometricspac": 6, "pseudoemetricspac": 6, "journei": 6, "recast": 6, "tendsto_attop": 6, "continuous_iff": 6, "devot": 6, "uncurri": 6, "slow": 6, "continuous_fst": 6, "comp": 6, "assembl": 6, "prod_mk": 6, "continuous_snd": 6, "continuous_dist": 6, "clunki": 6, "crucial": 6, "gradual": 6, "elabor": 6, "refus": 6, "prod_map": 6, "sad": 6, "wrap": 6, "border": 6, "obfusc": 6, "continuous_pow": 6, "continuous_id": 6, "continuousat": 6, "continuousat_iff": 6, "geometr": 6, "closedbal": 6, "radiu": 6, "mem_ball_self": 6, "mem_closedball_self": 6, "isopen": 6, "isopen_iff": 6, "Their": 6, "isclos": 6, "s\u1d9c": 6, "isopen_compl_iff": 6, "hu": 6, "mem_of_tendsto": 6, "mem_closure_iff": 6, "mem_closure_iff_seq_limit": 6, "main": 6, "nhds_basis_bal": 6, "nhds_basis_closedbal": 6, "mem_iff": 6, "segment": 6, "somewher": 6, "continuouson": 6, "minimum": 6, "deduc": 6, "iscompact": 6, "icc": 6, "iscompact_icc": 6, "\u03c6": 6, "strictmono": 6, "tendsto_subseq": 6, "exists_forall_l": 6, "exists_forall_g": 6, "compactspac": 6, "iscompact_univ": 6, "cauchi": 6, "uniformcontinu": 6, "uniformcontinuous_iff": 6, "clearli": 6, "isclosed_l": 6, "eq_empty_or_nonempti": 6, "attain": 6, "closer": 6, "cauchyseq": 6, "cauchyseq_iff": 6, "completespac": 6, "cauchyseq_tendsto_of_complet": 6, "criterion": 6, "explan": 6, "tendsto_pow_attop_nhds_0_of_lt_1": 6, "dist_le_range_sum_dist": 6, "cauchyseq_of_le_geometric_two": 6, "\u03b5_po": 6, "le_iff_exists_add": 6, "boss": 6, "bair": 6, "exclam": 6, "induct": [6, 10], "rec_on": 6, "ho": 6, "hd": 6, "dens": 6, "densiti": 6, "\u03b4po": 6, "hpo": 6, "hball": 6, "mem_closure_iff_nhds_basi": 6, "recon": 6, "rpo": 6, "rb": 6, "incl": 6, "cdist": 6, "ylim": 6, "yball": 6, "categor": 6, "ignor": 6, "topologicalspac": 6, "isopen_univ": 6, "isopen_empti": 6, "isopen_iunion": 6, "fintyp": 6, "isopen_iint": 6, "continuous_def": 6, "attach": 6, "filteri": 6, "sent": 6, "mem_nhds_iff": 6, "weird": 6, "digress": 6, "pure_le_nhd": 6, "eventually_eventually_nhd": 6, "topological_spac": 6, "mk_of_nhd": 6, "nhds_mk_of_nhd": 6, "clean": 6, "fonctori": 6, "induc": 6, "sensibl": 6, "uncount": 6, "relatedli": 6, "coinduc": 6, "t_x": 6, "t_y": 6, "coinduced_le_iff_le_induc": 6, "covari": 6, "coinduced_compos": 6, "induced_compos": 6, "topological_structur": 6, "primarili": 6, "ie": 6, "focus": 6, "nhd": 6, "opposit": 6, "recov": 6, "foward": 6, "continuous_iff_coinduced_l": 6, "g_": 6, "t_z": 6, "wasn": 6, "\u03c0": 6, "papar": 6, "t_": 6, "x_i": 6, "pi": 6, "defect": 6, "functori": 6, "price": 6, "patholog": 6, "t2_space": 6, "hausdorff": 6, "regular": 6, "t2space": 6, "tendsto_nhds_uniqu": 6, "regularspac": 6, "closed_nhds_basi": 6, "nhds_basis_open": 6, "denseinduc": 6, "continuousat_extend": 6, "funni": 6, "_in": 6, "thank": 6, "nhds_induc": 6, "is_open": 6, "fortiori": 6, "f_cont": 6, "tendsto_right_iff": 6, "firstcountabletopolog": 6, "sever": 6, "cluster": 6, "clusterpt": 6, "nebot": 6, "hfx": 6, "push_pul": 6, "of_map": 6, "f_ne": 6, "f_le": 6, "map_eq": 6, "hne": 6, "hle": 6, "huo": 6, "hsu": 6, "elim_finite_subcov": 6, "elementary_differential_calculu": 7, "introductori": 7, "normed_spac": 7, "overview": 10, "conjunct": 10, "converg": 10, "schr\u00f6der": 10, "bernstein": 10, "irrat": 10}, "objects": {}, "objtypes": {}, "objnames": {}, "titleterms": {"introduct": 0, "get": 0, "start": 0, "overview": 0, "basic": 1, "calcul": 1, "prove": 1, "ident": 1, "algebra": [1, 5], "structur": [1, 5], "us": 1, "theorem": [1, 3], "lemma": 1, "more": 1, "order": 1, "divis": 1, "fact": 1, "about": 1, "logic": 2, "implic": 2, "univers": 2, "quantifi": 2, "The": [2, 3], "existenti": 2, "negat": 2, "conjunct": 2, "bi": 2, "disjunct": 2, "sequenc": 2, "converg": [2, 6], "set": [3, 6], "function": [3, 6], "schr\u00f6der": 3, "bernstein": 3, "number": 4, "theori": [4, 8], "irrat": 4, "root": 4, "induct": 4, "recurs": 4, "infinit": 4, "mani": 4, "prime": 4, "abstract": 5, "build": 5, "gaussian": 5, "integ": 5, "topolog": 6, "filter": 6, "metric": 6, "space": 6, "continu": 6, "ball": 6, "open": 6, "close": 6, "compact": 6, "uniformli": 6, "complet": 6, "fundament": 6, "separ": 6, "countabl": 6, "differenti": 7, "calculu": 7, "integr": 8, "measur": 8, "index": 9, "mathemat": 10, "lean": 10}, "envversion": {"sphinx.domains.c": 2, "sphinx.domains.changeset": 1, "sphinx.domains.citation": 1, "sphinx.domains.cpp": 6, "sphinx.domains.index": 1, "sphinx.domains.javascript": 2, "sphinx.domains.math": 2, "sphinx.domains.python": 3, "sphinx.domains.rst": 2, "sphinx.domains.std": 2, "sphinx": 56}})