Date | Label | Description |
Theorem |
|
10-Apr-2025 | cndcap 14846 |
Real number trichotomy is equivalent to decidability of complex number
apartness. (Contributed by Jim Kingdon, 10-Apr-2025.)
|
 
 
   DECID
#   |
|
20-Mar-2025 | ccoslid 12692 |
Slot property of comp. (Contributed by Jim Kingdon, 20-Mar-2025.)
|
comp Slot
comp  comp 
  |
|
20-Mar-2025 | homslid 12690 |
Slot property of . (Contributed by Jim Kingdon, 20-Mar-2025.)
|
 Slot         |
|
19-Mar-2025 | ptex 12718 |
Existence of the product topology. (Contributed by Jim Kingdon,
19-Mar-2025.)
|
    
  |
|
18-Mar-2025 | prdsex 12723 |
Existence of the structure product. (Contributed by Jim Kingdon,
18-Mar-2025.)
|
     s
  |
|
13-Mar-2025 | imasex 12731 |
Existence of the image structure. (Contributed by Jim Kingdon,
13-Mar-2025.)
|
    s 
  |
|
11-Mar-2025 | imasival 12732 |
Value of an image structure. The is a lemma for the theorems
imasbas 12733, imasplusg 12734, and imasmulr 12735 and should not be needed once
they are proved. (Contributed by Mario Carneiro, 23-Feb-2015.)
(Revised by Jim Kingdon, 11-Mar-2025.) (New usage is discouraged.)
|
  s
          
        

                                  
                     
        
      
          |
|
8-Mar-2025 | subgex 13041 |
The class of subgroups of a group is a set. (Contributed by Jim
Kingdon, 8-Mar-2025.)
|
 SubGrp    |
|
28-Feb-2025 | ringressid 13243 |
A ring restricted to its base set is a ring. It will usually be the
original ring exactly, of course, but to show that needs additional
conditions such as those in strressid 12532. (Contributed by Jim Kingdon,
28-Feb-2025.)
|
     
↾s    |
|
28-Feb-2025 | grpressid 12936 |
A group restricted to its base set is a group. It will usually be the
original group exactly, of course, but to show that needs additional
conditions such as those in strressid 12532. (Contributed by Jim Kingdon,
28-Feb-2025.)
|
     
↾s    |
|
26-Feb-2025 | strext 12566 |
Extending the upper range of a structure. This works because when we
say that a structure has components in   we are
not saying
that every slot in that range is present, just that all the slots that
are present are within that range. (Contributed by Jim Kingdon,
26-Feb-2025.)
|
 Struct  
  
      Struct  
   |
|
23-Feb-2025 | ltlenmkv 14857 |
If can be
expressed as holding exactly when holds and the
values are not equal, then the analytic Markov's Principle applies. (To
get the regular Markov's Principle, combine with neapmkv 14855).
(Contributed by Jim Kingdon, 23-Feb-2025.)
|
 
    
  
#    |
|
23-Feb-2025 | neap0mkv 14856 |
The analytic Markov principle can be expressed either with two arbitrary
real numbers, or one arbitrary number and zero. (Contributed by Jim
Kingdon, 23-Feb-2025.)
|
 
  # 
 
#    |
|
23-Feb-2025 | lringuplu 13342 |
If the sum of two elements of a local ring is invertible, then at least
one of the summands must be invertible. (Contributed by Jim Kingdon,
18-Feb-2025.) (Revised by SN, 23-Feb-2025.)
|
       Unit         LRing          
   |
|
23-Feb-2025 | lringnz 13341 |
A local ring is a nonzero ring. (Contributed by Jim Kingdon,
20-Feb-2025.) (Revised by SN, 23-Feb-2025.)
|
        
LRing  |
|
23-Feb-2025 | lringring 13340 |
A local ring is a ring. (Contributed by Jim Kingdon, 20-Feb-2025.)
(Revised by SN, 23-Feb-2025.)
|
 LRing   |
|
23-Feb-2025 | lringnzr 13339 |
A local ring is a nonzero ring. (Contributed by SN, 23-Feb-2025.)
|
 LRing NzRing |
|
23-Feb-2025 | islring 13338 |
The predicate "is a local ring". (Contributed by SN, 23-Feb-2025.)
|
   
       Unit   LRing  NzRing      
     |
|
23-Feb-2025 | df-lring 13337 |
A local ring is a nonzero ring where for any two elements summing to
one, at least one is invertible. Any field is a local ring; the ring of
integers is an example of a ring which is not a local ring.
(Contributed by Jim Kingdon, 18-Feb-2025.) (Revised by SN,
23-Feb-2025.)
|
LRing  NzRing 
                        Unit  Unit      |
|
23-Feb-2025 | 01eq0ring 13335 |
If the zero and the identity element of a ring are the same, the ring is
the zero ring. (Contributed by AV, 16-Apr-2019.) (Proof shortened by
SN, 23-Feb-2025.)
|
                |
|
23-Feb-2025 | nzrring 13332 |
A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
(Proof shortened by SN, 23-Feb-2025.)
|
 NzRing   |
|
21-Feb-2025 | dftap2 7252 |
Tight apartness with the apartness properties from df-pap 7249 expanded.
(Contributed by Jim Kingdon, 21-Feb-2025.)
|
 TAp  
         
       
              
     |
|
20-Feb-2025 | aprap 13381 |
The relation given by df-apr 13376 for a local ring is an apartness
relation. (Contributed by Jim Kingdon, 20-Feb-2025.)
|
 LRing #r  Ap       |
|
20-Feb-2025 | setscomd 12505 |
Different components can be set in any order. (Contributed by Jim
Kingdon, 20-Feb-2025.)
|
               sSet
    sSet
      sSet     sSet
      |
|
17-Feb-2025 | aprcotr 13380 |
The apartness relation given by df-apr 13376 for a local ring is
cotransitive. (Contributed by Jim Kingdon, 17-Feb-2025.)
|
       # #r    LRing         #  # #     |
|
17-Feb-2025 | aprsym 13379 |
The apartness relation given by df-apr 13376 for a ring is symmetric.
(Contributed by Jim Kingdon, 17-Feb-2025.)
|
       # #r     
     # #    |
|
17-Feb-2025 | aprval 13377 |
Expand Definition df-apr 13376. (Contributed by Jim Kingdon,
17-Feb-2025.)
|
       # #r   
     
Unit   
       # 
    |
|
16-Feb-2025 | aprirr 13378 |
The apartness relation given by df-apr 13376 for a nonzero ring is
irreflexive. (Contributed by Jim Kingdon, 16-Feb-2025.)
|
       # #r     
            #   |
|
16-Feb-2025 | aptap 8609 |
Complex apartness (as defined at df-ap 8541) is a tight apartness (as
defined at df-tap 7251). (Contributed by Jim Kingdon, 16-Feb-2025.)
|
# TAp  |
|
15-Feb-2025 | tapeq2 7254 |
Equality theorem for tight apartness predicate. (Contributed by Jim
Kingdon, 15-Feb-2025.)
|
  TAp
TAp    |
|
14-Feb-2025 | exmidmotap 7262 |
The proposition that every class has at most one tight apartness is
equivalent to excluded middle. (Contributed by Jim Kingdon,
14-Feb-2025.)
|
EXMID    TAp   |
|
14-Feb-2025 | exmidapne 7261 |
Excluded middle implies there is only one tight apartness on any class,
namely negated equality. (Contributed by Jim Kingdon, 14-Feb-2025.)
|
EXMID  TAp
            |
|
14-Feb-2025 | df-pap 7249 |
Apartness predicate. A relation is an apartness if it is
irreflexive, symmetric, and cotransitive. (Contributed by Jim Kingdon,
14-Feb-2025.)
|
 Ap    
     
        
   
  
        |
|
13-Feb-2025 | df-apr 13376 |
The relation between elements whose difference is invertible, which for
a local ring is an apartness relation by aprap 13381. (Contributed by Jim
Kingdon, 13-Feb-2025.)
|
#r           
             Unit      |
|
8-Feb-2025 | 2oneel 7257 |
and are two unequal elements
of . (Contributed
by
Jim Kingdon, 8-Feb-2025.)
|
             |
|
8-Feb-2025 | tapeq1 7253 |
Equality theorem for tight apartness predicate. (Contributed by Jim
Kingdon, 8-Feb-2025.)
|
  TAp
TAp    |
|
6-Feb-2025 | 2omotap 7260 |
If there is at most one tight apartness on , excluded middle
follows. Based on online discussions by Tom de Jong, Andrew W Swan, and
Martin Escardo. (Contributed by Jim Kingdon, 6-Feb-2025.)
|
  TAp EXMID |
|
6-Feb-2025 | 2omotaplemst 7259 |
Lemma for 2omotap 7260. (Contributed by Jim Kingdon, 6-Feb-2025.)
|
   TAp 
  |
|
6-Feb-2025 | 2omotaplemap 7258 |
Lemma for 2omotap 7260. (Contributed by Jim Kingdon, 6-Feb-2025.)
|
            TAp   |
|
6-Feb-2025 | 2onetap 7256 |
Negated equality is a tight apartness on . (Contributed by Jim
Kingdon, 6-Feb-2025.)
|
         TAp  |
|
5-Feb-2025 | netap 7255 |
Negated equality on a set with decidable equality is a tight apartness.
(Contributed by Jim Kingdon, 5-Feb-2025.)
|
   DECID          TAp   |
|
5-Feb-2025 | df-tap 7251 |
Tight apartness predicate. A relation is a tight apartness if it
is irreflexive, symmetric, cotransitive, and tight. (Contributed by Jim
Kingdon, 5-Feb-2025.)
|
 TAp  Ap     
    |
|
1-Feb-2025 | mulgnn0cld 13009 |
Closure of the group multiple (exponentiation) operation for a
nonnegative multiplier in a monoid. Deduction associated with
mulgnn0cl 13004. (Contributed by SN, 1-Feb-2025.)
|
   
.g             |
|
31-Jan-2025 | 0subg 13064 |
The zero subgroup of an arbitrary group. (Contributed by Stefan O'Rear,
10-Dec-2014.) (Proof shortened by SN, 31-Jan-2025.)
|
     SubGrp    |
|
28-Jan-2025 | dvdsrex 13272 |
Existence of the divisibility relation. (Contributed by Jim Kingdon,
28-Jan-2025.)
|
 SRing  r    |
|
24-Jan-2025 | reldvdsrsrg 13266 |
The divides relation is a relation. (Contributed by Mario Carneiro,
1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2025.)
|
 SRing  r    |
|
18-Jan-2025 | rerecapb 8802 |
A real number has a multiplicative inverse if and only if it is apart
from zero. Theorem 11.2.4 of [HoTT], p.
(varies). (Contributed by Jim
Kingdon, 18-Jan-2025.)
|
  #  

   |
|
18-Jan-2025 | recapb 8630 |
A complex number has a multiplicative inverse if and only if it is apart
from zero. Theorem 11.2.4 of [HoTT], p.
(varies), generalized from
real to complex numbers. (Contributed by Jim Kingdon, 18-Jan-2025.)
|
  #  

   |
|
17-Jan-2025 | ressval3d 12533 |
Value of structure restriction, deduction version. (Contributed by AV,
14-Mar-2020.) (Revised by Jim Kingdon, 17-Jan-2025.)
|
 ↾s                    sSet       |
|
17-Jan-2025 | strressid 12532 |
Behavior of trivial restriction. (Contributed by Stefan O'Rear,
29-Nov-2014.) (Revised by Jim Kingdon, 17-Jan-2025.)
|
       Struct  
  
 
       ↾s 
  |
|
16-Jan-2025 | ressex 12527 |
Existence of structure restriction. (Contributed by Jim Kingdon,
16-Jan-2025.)
|
    ↾s    |
|
16-Jan-2025 | ressvalsets 12526 |
Value of structure restriction. (Contributed by Jim Kingdon,
16-Jan-2025.)
|
    ↾s   sSet                 |
|
10-Jan-2025 | opprex 13250 |
Existence of the opposite ring. If you know that is a ring, see
opprring 13254. (Contributed by Jim Kingdon, 10-Jan-2025.)
|
oppr     |
|
10-Jan-2025 | mgpex 13140 |
Existence of the multiplication group. If is known to be a
semiring, see srgmgp 13156. (Contributed by Jim Kingdon,
10-Jan-2025.)
|
mulGrp     |
|
5-Jan-2025 | imbibi 252 |
The antecedent of one side of a biconditional can be moved out of the
biconditional to become the antecedent of the remaining biconditional.
(Contributed by BJ, 1-Jan-2025.) (Proof shortened by Wolf Lammen,
5-Jan-2025.)
|
           |
|
1-Jan-2025 | snss 3729 |
The singleton of an element of a class is a subset of the class
(inference form of snssg 3728). Theorem 7.4 of [Quine] p. 49.
(Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ,
1-Jan-2025.)
|
     |
|
1-Jan-2025 | snssg 3728 |
The singleton formed on a set is included in a class if and only if the
set is an element of that class. Theorem 7.4 of [Quine] p. 49.
(Contributed by NM, 22-Jul-2001.) (Proof shortened by BJ, 1-Jan-2025.)
|
       |
|
1-Jan-2025 | snssb 3727 |
Characterization of the inclusion of a singleton in a class.
(Contributed by BJ, 1-Jan-2025.)
|
       |
|
9-Dec-2024 | nninfwlpoim 7178 |
Decidable equality for ℕ∞ implies the Weak Limited
Principle of
Omniscience (WLPO). (Contributed by Jim Kingdon, 9-Dec-2024.)
|
  ℕ∞  ℕ∞ DECID
WOmni |
|
8-Dec-2024 | nninfwlpoimlemdc 7177 |
Lemma for nninfwlpoim 7178. (Contributed by Jim Kingdon,
8-Dec-2024.)
|
                     ℕ∞ 
ℕ∞ DECID   DECID     
  |
|
8-Dec-2024 | nninfwlpoimlemginf 7176 |
Lemma for nninfwlpoim 7178. (Contributed by Jim Kingdon,
8-Dec-2024.)
|
                    
          |
|
8-Dec-2024 | nninfwlpoimlemg 7175 |
Lemma for nninfwlpoim 7178. (Contributed by Jim Kingdon,
8-Dec-2024.)
|
                    ℕ∞ |
|
7-Dec-2024 | nninfwlpor 7174 |
The Weak Limited Principle of Omniscience (WLPO) implies that equality
for ℕ∞ is decidable. (Contributed by Jim
Kingdon,
7-Dec-2024.)
|
 WOmni 
ℕ∞ 
ℕ∞ DECID   |
|
7-Dec-2024 | nninfwlporlem 7173 |
Lemma for nninfwlpor 7174. The result. (Contributed by Jim Kingdon,
7-Dec-2024.)
|
                  
        
WOmni  DECID
  |
|
6-Dec-2024 | nninfwlporlemd 7172 |
Given two countably infinite sequences of zeroes and ones, they are
equal if and only if a sequence formed by pointwise comparing them is
all ones. (Contributed by Jim Kingdon, 6-Dec-2024.)
|
                  
        

     |
|
3-Dec-2024 | nninfwlpo 7179 |
Decidability of equality for ℕ∞ is equivalent to the
Weak Limited
Principle of Omniscience (WLPO). (Contributed by Jim Kingdon,
3-Dec-2024.)
|
  ℕ∞  ℕ∞ DECID
WOmni |
|
3-Dec-2024 | nninfdcinf 7171 |
The Weak Limited Principle of Omniscience (WLPO) implies that it is
decidable whether an element of ℕ∞ equals the
point at infinity.
(Contributed by Jim Kingdon, 3-Dec-2024.)
|
 WOmni 
ℕ∞  DECID 
   |
|
28-Nov-2024 | basmexd 12524 |
A structure whose base is inhabited is a set. (Contributed by Jim
Kingdon, 28-Nov-2024.)
|
           |
|
22-Nov-2024 | eliotaeu 5207 |
An inhabited iota expression has a unique value. (Contributed by Jim
Kingdon, 22-Nov-2024.)
|
         |
|
22-Nov-2024 | eliota 5206 |
An element of an iota expression. (Contributed by Jim Kingdon,
22-Nov-2024.)
|
          
    |
|
18-Nov-2024 | basmex 12523 |
A structure whose base is inhabited is a set. (Contributed by Jim
Kingdon, 18-Nov-2024.)
|
       |
|
12-Nov-2024 | slotsdifipndx 12635 |
The slot for the scalar is not the index of other slots. (Contributed by
AV, 12-Nov-2024.)
|
    
    Scalar        |
|
11-Nov-2024 | bj-con1st 14542 |
Contraposition when the antecedent is a negated stable proposition. See
con1dc 856. (Contributed by BJ, 11-Nov-2024.)
|
STAB   
     |
|
11-Nov-2024 | slotsdifdsndx 12681 |
The index of the slot for the distance is not the index of other slots.
(Contributed by AV, 11-Nov-2024.)
|
                    |
|
11-Nov-2024 | slotsdifplendx 12670 |
The index of the slot for the distance is not the index of other slots.
(Contributed by AV, 11-Nov-2024.)
|
          TopSet        |
|
11-Nov-2024 | tsetndxnstarvndx 12654 |
The slot for the topology is not the slot for the involution in an
extensible structure. (Contributed by AV, 11-Nov-2024.)
|
TopSet        |
|
11-Nov-2024 | const 852 |
Contraposition when the antecedent is a negated stable proposition. See
comment of condc 853. (Contributed by BJ, 18-Nov-2023.) (Proof
shortened
by BJ, 11-Nov-2024.)
|
STAB  
      |
|
10-Nov-2024 | slotsdifunifndx 12688 |
The index of the slot for the uniform set is not the index of other slots.
(Contributed by AV, 10-Nov-2024.)
|
                          
                    |
|
7-Nov-2024 | ressbasd 12529 |
Base set of a structure restriction. (Contributed by Stefan O'Rear,
26-Nov-2014.) (Proof shortened by AV, 7-Nov-2024.)
|
 
↾s         
            |
|
6-Nov-2024 | oppraddg 13253 |
Addition operation of an opposite ring. (Contributed by Mario
Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.)
|
oppr           |
|
6-Nov-2024 | opprbasg 13252 |
Base set of an opposite ring. (Contributed by Mario Carneiro,
1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.)
|
oppr             |
|
6-Nov-2024 | opprsllem 13251 |
Lemma for opprbasg 13252 and oppraddg 13253. (Contributed by Mario Carneiro,
1-Dec-2014.) (Revised by AV, 6-Nov-2024.)
|
oppr   Slot             
        
      |
|
4-Nov-2024 | lgsfvalg 14445 |
Value of the function
which defines the Legendre symbol at the
primes. (Contributed by Mario Carneiro, 4-Feb-2015.) (Revised by Jim
Kingdon, 4-Nov-2024.)
|
  
                              
                    
 
                              
               |
|
1-Nov-2024 | plendxnvscandx 12669 |
The slot for the "less than or equal to" ordering is not the slot for
the
scalar product in an extensible structure. (Contributed by AV,
1-Nov-2024.)
|
         |
|
1-Nov-2024 | plendxnscandx 12668 |
The slot for the "less than or equal to" ordering is not the slot for
the
scalar in an extensible structure. (Contributed by AV, 1-Nov-2024.)
|
    Scalar   |
|
1-Nov-2024 | plendxnmulrndx 12667 |
The slot for the "less than or equal to" ordering is not the slot for
the
ring multiplication operation in an extensible structure. (Contributed by
AV, 1-Nov-2024.)
|
         |
|
1-Nov-2024 | qsqeqor 10633 |
The squares of two rational numbers are equal iff one number equals the
other or its negative. (Contributed by Jim Kingdon, 1-Nov-2024.)
|
                  |
|
31-Oct-2024 | dsndxnmulrndx 12678 |
The slot for the distance function is not the slot for the ring
multiplication operation in an extensible structure. (Contributed by AV,
31-Oct-2024.)
|
         |
|
31-Oct-2024 | tsetndxnmulrndx 12653 |
The slot for the topology is not the slot for the ring multiplication
operation in an extensible structure. (Contributed by AV,
31-Oct-2024.)
|
TopSet       |
|
31-Oct-2024 | tsetndxnbasendx 12651 |
The slot for the topology is not the slot for the base set in an
extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened
by AV, 31-Oct-2024.)
|
TopSet       |
|
31-Oct-2024 | basendxlttsetndx 12650 |
The index of the slot for the base set is less then the index of the slot
for the topology in an extensible structure. (Contributed by AV,
31-Oct-2024.)
|
    TopSet   |
|
31-Oct-2024 | tsetndxnn 12649 |
The index of the slot for the group operation in an extensible structure
is a positive integer. (Contributed by AV, 31-Oct-2024.)
|
TopSet   |
|
30-Oct-2024 | plendxnbasendx 12665 |
The slot for the order is not the slot for the base set in an extensible
structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV,
30-Oct-2024.)
|
         |
|
30-Oct-2024 | basendxltplendx 12664 |
The index value of the slot is less than the index value of the
slot.
(Contributed by AV, 30-Oct-2024.)
|
         |
|
30-Oct-2024 | plendxnn 12663 |
The index value of the order slot is a positive integer. This property
should be ensured for every concrete coding because otherwise it could not
be used in an extensible structure (slots must be positive integers).
(Contributed by AV, 30-Oct-2024.)
|
   
 |
|
29-Oct-2024 | dsndxntsetndx 12680 |
The slot for the distance function is not the slot for the topology in an
extensible structure. (Contributed by AV, 29-Oct-2024.)
|
    TopSet   |
|
29-Oct-2024 | slotsdnscsi 12679 |
The slots Scalar,
and are different
from the slot
.
(Contributed by AV, 29-Oct-2024.)
|
     Scalar         
          |
|
29-Oct-2024 | slotstnscsi 12655 |
The slots Scalar,
and are different
from the slot
TopSet. (Contributed by AV, 29-Oct-2024.)
|
 TopSet  Scalar  TopSet     
TopSet        |
|
29-Oct-2024 | ipndxnmulrndx 12634 |
The slot for the inner product is not the slot for the ring
(multiplication) operation in an extensible structure. (Contributed by
AV, 29-Oct-2024.)
|
         |
|
29-Oct-2024 | ipndxnplusgndx 12633 |
The slot for the inner product is not the slot for the group operation in
an extensible structure. (Contributed by AV, 29-Oct-2024.)
|
        |