Point-free Construction of Real Exponentiation HVGT9D84WV
| URI | m2://res/HVGT9D84WV |
|---|---|
| Kind | preprint |
| Creators | Ming Ng, Steven Vickers |
| Date | 2021-03-31 |
| MSC | 18-XX |
| Subjects | arxiv math.CT |
| Scope | in |
Expressions
e1: version, preprint
| Language | en |
|---|---|
| Date | 2021-03-31 |
| Ids | arXiv 2104.00162, DOI 10.46298/lmcs-18(3:15)2022 |
Items in this resource
The mentions of the inventory that name this resource. Each name links to the card of its inventory row.
| Item | Kind | Where | Source |
|---|---|---|---|
| 181EC0GSBY | definition | definition 1.5 | arxiv |
| 1AMYA2B8EX | statement | lemma 3.8 | arxiv |
| 1VE16P7P3T | definition | definition 1.4 | arxiv |
| 20CERRAZ6E | definition | definition 1.34 | arxiv |
| 2JVCC62TK4 | statement | proposition 1.8 | arxiv |
| Conservativity of the generic model | statement | fact 1.10 | arxiv |
| 2PZ5FVD4GA | statement | lemma 2.14 | arxiv |
| 2Y7EN03CH2 | definition | definition 1.18 | arxiv |
| 4DP2SX81ZW | statement | lemma 1.26 | arxiv |
| 4T5Q8TPFHM | statement | fact 4.3 | arxiv |
| 554KHNJYKM | statement | corollary 2.10 | arxiv |
| 58757CC2AK | statement | corollary 3.11 | arxiv |
| 5PC9P21NT4 | definition | definition 1.3 | arxiv |
| 5V1PCZBZGP | statement | proposition 1.36 | arxiv |
| 666K5STXQB | statement | theorem 3.12 | arxiv |
| 7W5TQFZAVM | statement | theorem 3.5 | arxiv |
| ``Fixing $x$'' | definition | definition 1.9 | arxiv |
| 9GYE1V7B2S | definition | definition 1.33 | arxiv |
| 9P15GA1G92 | statement | proposition 1.13 | arxiv |
| 9T3B7V20MD | statement | proposition 2.17 | arxiv |
| Lifting Lemma | statement | lemma 1.29 | arxiv |
| ATJS55XA4R | definition | definition 1.12 | arxiv |
| AXE0G1FGH0 | statement | corollary 3.10 | arxiv |
| B4SRX6TCEX | statement | proposition 2.8 | arxiv |
| B8V822X84J | definition | definition 1.24 | arxiv |
| BPGM5EFZBM | statement | fact 1.25 | arxiv |
| BY5XT2GH9A | statement | proposition 3.4 | arxiv |
| DCZDRP8665 | statement | proposition 2.4 | arxiv |
| DFVGZRTDWY | definition | definition 1.11 | arxiv |
| DK6WM6G15G | statement | lemma 4.1 | arxiv |
| ED95S6Y4CE | definition | definition 1.28 | arxiv |
| EFXH9M8GWA | statement | proposition 2.16 | arxiv |
| Monotonicity | statement | lemma 2.7 | arxiv |
| F99T1JYS8K | statement | lemma 2.3 | arxiv |
| FM9MRKFBA7 | statement | proposition 2.5 | arxiv |
| FR81ZK2C5D | definition | definition 1.15 | arxiv |
| GDPCH1NF3N | definition | definition 1.32 | arxiv |
| J8RRSWV7KP | definition | definition 1.31 | arxiv |
| JGSR6NTWN3 | statement | proposition 2.11 | arxiv |
| Monotone/Antitone behaviour of rational exponents | statement | proposition 3.1 | arxiv |
| Continuity Lemma | statement | lemma 3.3 | arxiv |
| K48M4A53ZK | statement | proposition 2.18 | arxiv |
| MCKDEDZCJY | statement | proposition 2.1 | arxiv |
| Bernoulli's Inequality | statement | lemma 3.2 | arxiv |
| Point-free vs. Point-set Topology | definition | definition 1.1 | arxiv |
| Archimedean Property | statement | fact 1.17 | arxiv |
| QFFGQY4F56 | definition | definition 1.22 | arxiv |
| S22H6017D7 | definition | definition 1.23 | arxiv |
| Gluing Principle | statement | proposition 1.37 | arxiv |
| V9Z1JBND6C | statement | theorem 3.9 | arxiv |
| VN2JDKYYFR | definition | definition 2.13 | arxiv |
| W820Z9DNPQ | definition | definition 1.14 | arxiv |
| Monotonicity | statement | lemma 2.2 | arxiv |
| XF7MYZ3BNW | definition | definition 1.21 | arxiv |
| Y0XW19J9ZM | statement | proposition 2.9 | arxiv |
| Y6FZF8Y7B0 | statement | theorem 4.2 | arxiv |
| Y6WGCYCFB1 | statement | corollary 1.27 | arxiv |
| YEQED54VYS | statement | corollary 1.38 | arxiv |
| YPPE1523BE | example | example 1.6 | arxiv |
| YV09BTE273 | definition | definition 1.7 | arxiv |
| Geometricity | definition | definition 1.2 | arxiv |
| ``Non-negative Reals'' | definition | definition 2.6 | arxiv |
| ZB3GYT6GRW | statement | corollary 3.7 | arxiv |
| ZKN117K272 | statement | lemma 2.12 | arxiv |
Catalogue records
- arxiv: 2104.00162 (work)
- arxiv_text: 2104.00162 (work)