Home | Intuitionistic Logic Explorer Theorem List (p. 120 of 133) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | phicld 11901 | Closure for the value of the Euler function. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | phi1 11902 | Value of the Euler function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.) |
Theorem | dfphi2 11903* | Alternate definition of the Euler function. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 2-May-2016.) |
♯ ..^ | ||
Theorem | hashdvds 11904* | The number of numbers in a given residue class in a finite set of integers. (Contributed by Mario Carneiro, 12-Mar-2014.) (Proof shortened by Mario Carneiro, 7-Jun-2016.) |
♯ | ||
Theorem | phiprmpw 11905 | Value of the Euler function at a prime power. Theorem 2.5(a) in [ApostolNT] p. 28. (Contributed by Mario Carneiro, 24-Feb-2014.) |
Theorem | phiprm 11906 | Value of the Euler function at a prime. (Contributed by Mario Carneiro, 28-Feb-2014.) |
Theorem | crth 11907* | The Chinese Remainder Theorem: the function that maps to its remainder classes and is 1-1 and onto when and are coprime. (Contributed by Mario Carneiro, 24-Feb-2014.) (Proof shortened by Mario Carneiro, 2-May-2016.) |
..^ ..^ ..^ | ||
Theorem | phimullem 11908* | Lemma for phimul 11909. (Contributed by Mario Carneiro, 24-Feb-2014.) |
..^ ..^ ..^ ..^ ..^ | ||
Theorem | phimul 11909 | The Euler function is a multiplicative function, meaning that it distributes over multiplication at relatively prime arguments. Theorem 2.5(c) in [ApostolNT] p. 28. (Contributed by Mario Carneiro, 24-Feb-2014.) |
Theorem | hashgcdlem 11910* | A correspondence between elements of specific GCD and relative primes in a smaller ring. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
..^ ..^ | ||
Theorem | hashgcdeq 11911* | Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
♯ ..^ | ||
Theorem | oddennn 11912 | There are as many odd positive integers as there are positive integers. (Contributed by Jim Kingdon, 11-May-2022.) |
Theorem | evenennn 11913 | There are as many even positive integers as there are positive integers. (Contributed by Jim Kingdon, 12-May-2022.) |
Theorem | xpnnen 11914 | The Cartesian product of the set of positive integers with itself is equinumerous to the set of positive integers. (Contributed by NM, 1-Aug-2004.) |
Theorem | xpomen 11915 | The Cartesian product of omega (the set of ordinal natural numbers) with itself is equinumerous to omega. Exercise 1 of [Enderton] p. 133. (Contributed by NM, 23-Jul-2004.) |
Theorem | xpct 11916 | The cartesian product of two sets dominated by is dominated by . (Contributed by Thierry Arnoux, 24-Sep-2017.) |
Theorem | unennn 11917 | The union of two disjoint countably infinite sets is countably infinite. (Contributed by Jim Kingdon, 13-May-2022.) |
Theorem | znnen 11918 | The set of integers and the set of positive integers are equinumerous. Corollary 8.1.23 of [AczelRathjen], p. 75. (Contributed by NM, 31-Jul-2004.) |
Theorem | ennnfonelemdc 11919* | Lemma for ennnfone 11945. A direct consequence of fidcenumlemrk 6842. (Contributed by Jim Kingdon, 15-Jul-2023.) |
DECID DECID | ||
Theorem | ennnfonelemk 11920* | Lemma for ennnfone 11945. (Contributed by Jim Kingdon, 15-Jul-2023.) |
Theorem | ennnfonelemj0 11921* | Lemma for ennnfone 11945. Initial state for . (Contributed by Jim Kingdon, 20-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemjn 11922* | Lemma for ennnfone 11945. Non-initial state for . (Contributed by Jim Kingdon, 20-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemg 11923* | Lemma for ennnfone 11945. Closure for . (Contributed by Jim Kingdon, 20-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemh 11924* | Lemma for ennnfone 11945. (Contributed by Jim Kingdon, 8-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelem0 11925* | Lemma for ennnfone 11945. Initial value. (Contributed by Jim Kingdon, 15-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemp1 11926* | Lemma for ennnfone 11945. Value of at a successor. (Contributed by Jim Kingdon, 23-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelem1 11927* | Lemma for ennnfone 11945. Second value. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemom 11928* | Lemma for ennnfone 11945. yields finite sequences. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemhdmp1 11929* | Lemma for ennnfone 11945. Domain at a successor where we need to add an element to the sequence. (Contributed by Jim Kingdon, 23-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemss 11930* | Lemma for ennnfone 11945. We only add elements to as the index increases. (Contributed by Jim Kingdon, 15-Jul-2023.) |
DECID frec | ||
Theorem | ennnfoneleminc 11931* | Lemma for ennnfone 11945. We only add elements to as the index increases. (Contributed by Jim Kingdon, 21-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemkh 11932* | Lemma for ennnfone 11945. Because we add zero or one entries for each new index, the length of each sequence is no greater than its index. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemhf1o 11933* | Lemma for ennnfone 11945. Each of the functions in is one to one and onto an image of . (Contributed by Jim Kingdon, 17-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemex 11934* | Lemma for ennnfone 11945. Extending the sequence to include an additional element. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemhom 11935* | Lemma for ennnfone 11945. The sequences in increase in length without bound if you go out far enough. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemrnh 11936* | Lemma for ennnfone 11945. A consequence of ennnfonelemss 11930. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemfun 11937* | Lemma for ennnfone 11945. is a function. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemf1 11938* | Lemma for ennnfone 11945. is one-to-one. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemrn 11939* | Lemma for ennnfone 11945. is onto . (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemdm 11940* | Lemma for ennnfone 11945. The function is defined everywhere. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemen 11941* | Lemma for ennnfone 11945. The result. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemnn0 11942* | Lemma for ennnfone 11945. A version of ennnfonelemen 11941 expressed in terms of instead of . (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID frec | ||
Theorem | ennnfonelemr 11943* | Lemma for ennnfone 11945. The interesting direction, expressed in deduction form. (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID | ||
Theorem | ennnfonelemim 11944* | Lemma for ennnfone 11945. The trivial direction. (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID | ||
Theorem | ennnfone 11945* | A condition for a set being countably infinite. Corollary 8.1.13 of [AczelRathjen], p. 73. Roughly speaking, the condition says that is countable (that's the part, as seen in theorems like ctm 6994), infinite (that's the part about being able to find an element of distinct from any mapping of a natural number via ), and has decidable equality. (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID | ||
Theorem | exmidunben 11946* | If any unbounded set of positive integers is equinumerous to , then the Limited Principle of Omniscience (LPO) implies excluded middle. (Contributed by Jim Kingdon, 29-Jul-2023.) |
Omni EXMID | ||
Theorem | ctinfomlemom 11947* | Lemma for ctinfom 11948. Converting between and . (Contributed by Jim Kingdon, 10-Aug-2023.) |
frec | ||
Theorem | ctinfom 11948* | A condition for a set being countably infinite. Restates ennnfone 11945 in terms of and function image. Like ennnfone 11945 the condition can be summarized as being countable, infinite, and having decidable equality. (Contributed by Jim Kingdon, 7-Aug-2023.) |
DECID | ||
Theorem | inffinp1 11949* | An infinite set contains an element not contained in a given finite subset. (Contributed by Jim Kingdon, 7-Aug-2023.) |
DECID | ||
Theorem | ctinf 11950* | A set is countably infinite if and only if it has decidable equality, is countable, and is infinite. (Contributed by Jim Kingdon, 7-Aug-2023.) |
DECID | ||
Theorem | qnnen 11951 | The rational numbers are countably infinite. Corollary 8.1.23 of [AczelRathjen], p. 75. This is Metamath 100 proof #3. (Contributed by Jim Kingdon, 11-Aug-2023.) |
Theorem | enctlem 11952* | Lemma for enct 11953. One direction of the biconditional. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ ⊔ | ||
Theorem | enct 11953* | Countability is invariant relative to equinumerosity. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ ⊔ | ||
Theorem | ctiunctlemu1st 11954* | Lemma for ctiunct 11960. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunctlemu2nd 11955* | Lemma for ctiunct 11960. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunctlemuom 11956 | Lemma for ctiunct 11960. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunctlemudc 11957* | Lemma for ctiunct 11960. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID DECID | ||
Theorem | ctiunctlemf 11958* | Lemma for ctiunct 11960. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunctlemfo 11959* | Lemma for ctiunct 11960. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunct 11960* |
A sequence of enumerations gives an enumeration of the union. We refer
to "sequence of enumerations" rather than "countably many
countable
sets" because the hypothesis provides more than countability for
each
: it refers to together with the
which enumerates it. Theorem 8.1.19 of [AczelRathjen], p. 74.
The "countably many countable sets" version could be expressed as ⊔ and countable choice (or something similar) would be needed to derive the current hypothesis from that. Compare with the case of two sets instead of countably many, as seen at unct 11962, in which case we express countability using . The proof proceeds by mapping a natural number to a pair of natural numbers (by xpomen 11915) and using the first number to map to an element of and the second number to map to an element of B(x) . In this way we are able to map to every element of . Although it would be possible to work directly with countability expressed as ⊔ , we instead use functions from subsets of the natural numbers via ctssdccl 6996 and ctssdc 6998. (Contributed by Jim Kingdon, 31-Oct-2023.) |
⊔ ⊔ ⊔ | ||
Theorem | ctiunctal 11961* | Variation of ctiunct 11960 which allows to be present in . (Contributed by Jim Kingdon, 5-May-2024.) |
⊔ ⊔ ⊔ | ||
Theorem | unct 11962* | The union of two countable sets is countable. Corollary 8.1.20 of [AczelRathjen], p. 75. (Contributed by Jim Kingdon, 1-Nov-2023.) |
⊔ ⊔ ⊔ | ||
Theorem | omctfn 11963* | Using countable choice to find a sequence of enumerations for a collection of countable sets. Lemma 8.1.27 of [AczelRathjen], p. 77. (Contributed by Jim Kingdon, 19-Apr-2024.) |
CCHOICE ⊔ ⊔ | ||
Theorem | omiunct 11964* | The union of a countably infinite collection of countable sets is countable. Theorem 8.1.28 of [AczelRathjen], p. 78. Compare with ctiunct 11960 which has a stronger hypothesis but does not require countable choice. (Contributed by Jim Kingdon, 5-May-2024.) |
CCHOICE ⊔ ⊔ | ||
An "extensible structure" (or "structure" in short, at least in this section) is used to define a specific group, ring, poset, and so on. An extensible structure can contain many components. For example, a group will have at least two components (base set and operation), although it can be further specialized by adding other components such as a multiplicative operation for rings (and still remain a group per our definition). Thus, every ring is also a group. This extensible structure approach allows theorems from more general structures (such as groups) to be reused for more specialized structures (such as rings) without having to reprove anything. Structures are common in mathematics, but in informal (natural language) proofs the details are assumed in ways that we must make explicit. An extensible structure is implemented as a function (a set of ordered pairs) on a finite (and not necessarily sequential) subset of . The function's argument is the index of a structure component (such as for the base set of a group), and its value is the component (such as the base set). By convention, we normally avoid direct reference to the hard-coded numeric index and instead use structure component extractors such as ndxid 11993 and strslfv 12013. Using extractors makes it easier to change numeric indices and also makes the components' purpose clearer. There are many other possible ways to handle structures. We chose this extensible structure approach because this approach (1) results in simpler notation than other approaches we are aware of, and (2) is easier to do proofs with. We cannot use an approach that uses "hidden" arguments; Metamath does not support hidden arguments, and in any case we want nothing hidden. It would be possible to use a categorical approach (e.g., something vaguely similar to Lean's mathlib). However, instances (the chain of proofs that an is a via a bunch of forgetful functors) can cause serious performance problems for automated tooling, and the resulting proofs would be painful to look at directly (in the case of Lean, they are long past the level where people would find it acceptable to look at them directly). Metamath is working under much stricter conditions than this, and it has still managed to achieve about the same level of flexibility through this "extensible structure" approach. To create a substructure of a given extensible structure, you can simply use the multifunction restriction operator for extensible structures ↾_{s} as defined in df-ress 11977. This can be used to turn statements about rings into statements about subrings, modules into submodules, etc. This definition knows nothing about individual structures and merely truncates the set while leaving operators alone. Individual kinds of structures will need to handle this behavior by ignoring operators' values outside the range, defining a function using the base set and applying that, or explicitly truncating the slot before use. Extensible structures only work well when they represent concrete categories, where there is a "base set", morphisms are functions, and subobjects are subsets with induced operations. In short, they primarily work well for "sets with (some) extra structure". Extensible structures may not suffice for more complicated situations. For example, in manifolds, ↾_{s} would not work. That said, extensible structures are sufficient for many of the structures that set.mm currently considers, and offer a good compromise for a goal-oriented formalization. | ||
Syntax | cstr 11965 | Extend class notation with the class of structures with components numbered below . |
Struct | ||
Syntax | cnx 11966 | Extend class notation with the structure component index extractor. |
Syntax | csts 11967 | Set components of a structure. |
sSet | ||
Syntax | cslot 11968 | Extend class notation with the slot function. |
Slot | ||
Syntax | cbs 11969 | Extend class notation with the class of all base set extractors. |
Syntax | cress 11970 | Extend class notation with the extensible structure builder restriction operator. |
↾_{s} | ||
Definition | df-struct 11971* |
Define a structure with components in . This is
not a
requirement for groups, posets, etc., but it is a useful assumption for
component extraction theorems.
As mentioned in the section header, an "extensible structure should be implemented as a function (a set of ordered pairs)". The current definition, however, is less restrictive: it allows for classes which contain the empty set to be extensible structures. Because of 0nelfun 5141, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 11982: Struct . Allowing an extensible structure to contain the empty set ensures that expressions like are structures without asserting or implying that , , and are sets (if or is a proper class, then , see opprc 3726). (Contributed by Mario Carneiro, 29-Aug-2015.) |
Struct | ||
Definition | df-ndx 11972 | Define the structure component index extractor. See theorem ndxarg 11992 to understand its purpose. The restriction to ensures that is a set. The restriction to some set is necessary since is a proper class. In principle, we could have chosen or (if we revise all structure component definitions such as df-base 11975) another set such as the set of finite ordinals (df-iom 4505). (Contributed by NM, 4-Sep-2011.) |
Definition | df-slot 11973* |
Define the slot extractor for extensible structures. The class
Slot is a
function whose argument can be any set, although it is
meaningful only if that set is a member of an extensible structure (such
as a partially ordered set or a group).
Note that Slot is implemented as "evaluation at ". That is, Slot is defined to be , where will typically be a small nonzero natural number. Each extensible structure is a function defined on specific natural number "slots", and this function extracts the value at a particular slot. The special "structure" , defined as the identity function restricted to , can be used to extract the number from a slot, since Slot (see ndxarg 11992). This is typically used to refer to the number of a slot when defining structures without having to expose the detail of what that number is (for instance, we use the expression in theorems and proofs instead of its value 1). The class Slot cannot be defined as because each Slot is a function on the proper class so is itself a proper class, and the values of functions are sets (fvex 5441). It is necessary to allow proper classes as values of Slot since for instance the class of all (base sets of) groups is proper. (Contributed by Mario Carneiro, 22-Sep-2015.) |
Slot | ||
Theorem | sloteq 11974 | Equality theorem for the Slot construction. The converse holds if (or ) is a set. (Contributed by BJ, 27-Dec-2021.) |
Slot Slot | ||
Definition | df-base 11975 | Define the base set (also called underlying set, ground set, carrier set, or carrier) extractor for extensible structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
Slot | ||
Definition | df-sets 11976* | Set a component of an extensible structure. This function is useful for taking an existing structure and "overriding" one of its components. For example, df-ress 11977 adjusts the base set to match its second argument, which has the effect of making subgroups, subspaces, subrings etc. from the original structures. (Contributed by Mario Carneiro, 1-Dec-2014.) |
sSet | ||
Definition | df-ress 11977* |
Define a multifunction restriction operator for extensible structures,
which can be used to turn statements about rings into statements about
subrings, modules into submodules, etc. This definition knows nothing
about individual structures and merely truncates the set while
leaving operators alone; individual kinds of structures will need to
handle this behavior, by ignoring operators' values outside the range,
defining a function using the base set and applying that, or explicitly
truncating the slot before use.
(Credit for this operator goes to Mario Carneiro.) (Contributed by Stefan O'Rear, 29-Nov-2014.) |
↾_{s} sSet | ||
Theorem | brstruct 11978 | The structure relation is a relation. (Contributed by Mario Carneiro, 29-Aug-2015.) |
Struct | ||
Theorem | isstruct2im 11979 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
Theorem | isstruct2r 11980 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
Theorem | structex 11981 | A structure is a set. (Contributed by AV, 10-Nov-2021.) |
Struct | ||
Theorem | structn0fun 11982 | A structure without the empty set is a function. (Contributed by AV, 13-Nov-2021.) |
Struct | ||
Theorem | isstructim 11983 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
Theorem | isstructr 11984 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
Theorem | structcnvcnv 11985 | Two ways to express the relational part of a structure. (Contributed by Mario Carneiro, 29-Aug-2015.) |
Struct | ||
Theorem | structfung 11986 | The converse of the converse of a structure is a function. Closed form of structfun 11987. (Contributed by AV, 12-Nov-2021.) |
Struct | ||
Theorem | structfun 11987 | Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Proof shortened by AV, 12-Nov-2021.) |
Struct | ||
Theorem | structfn 11988 | Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.) |
Struct | ||
Theorem | strnfvnd 11989 | Deduction version of strnfvn 11990. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 19-Jan-2023.) |
Slot | ||
Theorem | strnfvn 11990 |
Value of a structure component extractor . Normally, is a
defined constant symbol such as (df-base 11975) and is a
fixed integer such as . is a
structure, i.e. a specific
member of a class of structures.
Note: Normally, this theorem shouldn't be used outside of this section, because it requires hard-coded index values. Instead, use strslfv 12013. (Contributed by NM, 9-Sep-2011.) (Revised by Jim Kingdon, 19-Jan-2023.) (New usage is discouraged.) |
Slot | ||
Theorem | strfvssn 11991 | A structure component extractor produces a value which is contained in a set dependent on , but not . This is sometimes useful for showing sethood. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Jim Kingdon, 19-Jan-2023.) |
Slot | ||
Theorem | ndxarg 11992 | Get the numeric argument from a defined structure component extractor such as df-base 11975. (Contributed by Mario Carneiro, 6-Oct-2013.) |
Slot | ||
Theorem | ndxid 11993 |
A structure component extractor is defined by its own index. This
theorem, together with strslfv 12013 below, is useful for avoiding direct
reference to the hard-coded numeric index in component extractor
definitions, such as the in df-base 11975, making it easier to change
should the need arise.
(Contributed by NM, 19-Oct-2012.) (Revised by Mario Carneiro, 6-Oct-2013.) (Proof shortened by BJ, 27-Dec-2021.) |
Slot Slot | ||
Theorem | ndxslid 11994 | A structure component extractor is defined by its own index. That the index is a natural number will also be needed in quite a few contexts so it is included in the conclusion of this theorem which can be used as a hypothesis of theorems like strslfv 12013. (Contributed by Jim Kingdon, 29-Jan-2023.) |
Slot Slot | ||
Theorem | slotslfn 11995 | A slot is a function on sets, treated as structures. (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by Jim Kingdon, 10-Feb-2023.) |
Slot | ||
Theorem | slotex 11996 | Existence of slot value. A corollary of slotslfn 11995. (Contributed by Jim Kingdon, 12-Feb-2023.) |
Slot | ||
Theorem | strndxid 11997 | The value of a structure component extractor is the value of the corresponding slot of the structure. (Contributed by AV, 13-Mar-2020.) |
Slot | ||
Theorem | reldmsets 11998 | The structure override operator is a proper operator. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
sSet | ||
Theorem | setsvalg 11999 | Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015.) |
sSet | ||
Theorem | setsvala 12000 | Value of the structure replacement function. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 20-Jan-2023.) |
sSet |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |