Grothendieck Universes
The foundation of the Mizar Mathematical Library [2], is first-order Tarski-Grothendieck set theory. However, the foundation explicitly refers only to Tarski’s Axiom A, which states that for every set X there is a Tarski universe U such that X ∈ U. In this article, we prove, using the Mizar [3] form...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Sciendo
2020-07-01
|
| Series: | Formalized Mathematics |
| Subjects: | |
| Online Access: | https://doi.org/10.2478/forma-2020-0018 |