![]() |
Metamath
Proof Explorer Theorem List (p. 337 of 437) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28347) |
![]() (28348-29872) |
![]() (29873-43639) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-evalid 33601 | The evaluation at a set of the identity function is that set. (General form of ndxarg 16280.) The restriction to a set 𝑉 is necessary since the argument of the function Slot 𝐴 (like that of any function) has to be a set for the evaluation to be meaningful. (Contributed by BJ, 27-Dec-2021.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → (Slot 𝐴‘( I ↾ 𝑉)) = 𝐴) | ||
Theorem | bj-ndxarg 33602 | Proof of ndxarg 16280 from bj-evalid 33601. (Contributed by BJ, 27-Dec-2021.) (Proof modification is discouraged.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝐸‘ndx) = 𝑁 | ||
Theorem | bj-ndxid 33603 | Proof of ndxid 16281 from ndxarg 16280. (Contributed by BJ, 27-Dec-2021.) (Proof modification is discouraged.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ 𝐸 = Slot (𝐸‘ndx) | ||
Theorem | bj-evalidval 33604 | Closed general form of strndxid 16282. Both sides are equal to (𝐹‘𝐴) by bj-evalid 33601 and bj-evalval 33600 respectively, but bj-evalidval 33604 adds something to bj-evalid 33601 and bj-evalval 33600 in that Slot 𝐴 appears on both sides. (Contributed by BJ, 27-Dec-2021.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑈) → (𝐹‘(Slot 𝐴‘( I ↾ 𝑉))) = (Slot 𝐴‘𝐹)) | ||
Syntax | celwise 33605 | Syntax for elementwise operations. |
class elwise | ||
Definition | df-elwise 33606* | Define the elementwise operation associated with a given operation. For instance, + is the addition of complex numbers (axaddf 10302), so if 𝐴 and 𝐵 are sets of complex numbers, then (𝐴(elwise‘ + )𝐵) is the set of numbers of the form (𝑥 + 𝑦) with 𝑥 ∈ 𝐴 and 𝑦 ∈ 𝐵. The set of odd natural numbers is (({2}(elwise‘ · )ℕ0)(elwise‘ + ){1}), or less formally 2ℕ0 + 1. (Contributed by BJ, 22-Dec-2021.) |
⊢ elwise = (𝑜 ∈ V ↦ (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∣ ∃𝑢 ∈ 𝑥 ∃𝑣 ∈ 𝑦 𝑧 = (𝑢𝑜𝑣)})) | ||
Many kinds of structures are given by families of subsets of a given set: Moore collections (df-mre 16632), topologies (df-top 21106), pi-systems, rings of sets, delta-rings, lambda-systems/Dynkin systems, algebras/fields of sets, sigma-algebras/sigma-fields/tribes (df-siga 30769), sigma rings, monotone classes, matroids/independent sets, bornologies, filters. There is a natural notion of structure induced on a subset. It is often given by an elementwise intersection, namely, the family of intersections of sets in the original family with the given subset. In this subsection, we define this notion and prove its main properties. Classical conditions on families of subsets include being nonempty, containing the whole set, containing the empty set, being stable under unions, intersections, subsets, supersets, (relative) complements. Therefore, we prove related properties for the elementwise intersection. We will call (𝑋 ↾t 𝐴) the elementwise intersection on the family 𝑋 by the class 𝐴. REMARK: many theorems are already in set.mm ; MM> SEARCH *rest* / JOIN | ||
Theorem | bj-rest00 33607 | An elementwise intersection on the empty family is the empty set. TODO: this is 0rest 16476. (Contributed by BJ, 27-Apr-2021.) |
⊢ (∅ ↾t 𝐴) = ∅ | ||
Theorem | bj-restsn 33608 | An elementwise intersection on the singleton on a set is the singleton on the intersection by that set. Generalization of bj-restsn0 33611 and bj-restsnid 33613. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ({𝑌} ↾t 𝐴) = {(𝑌 ∩ 𝐴)}) | ||
Theorem | bj-restsnss 33609 | Special case of bj-restsn 33608. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑌) → ({𝑌} ↾t 𝐴) = {𝐴}) | ||
Theorem | bj-restsnss2 33610 | Special case of bj-restsn 33608. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ⊆ 𝐴) → ({𝑌} ↾t 𝐴) = {𝑌}) | ||
Theorem | bj-restsn0 33611 | An elementwise intersection on the singleton on the empty set is the singleton on the empty set. Special case of bj-restsn 33608 and bj-restsnss2 33610. TODO: this is restsn 21382. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝐴 ∈ 𝑉 → ({∅} ↾t 𝐴) = {∅}) | ||
Theorem | bj-restsn10 33612 | Special case of bj-restsn 33608, bj-restsnss 33609, and bj-rest10 33614. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ 𝑉 → ({𝑋} ↾t ∅) = {∅}) | ||
Theorem | bj-restsnid 33613 | The elementwise intersection on the singleton on a class by that class is the singleton on that class. Special case of bj-restsn 33608 and bj-restsnss 33609. (Contributed by BJ, 27-Apr-2021.) |
⊢ ({𝐴} ↾t 𝐴) = {𝐴} | ||
Theorem | bj-rest10 33614 | An elementwise intersection on a nonempty family by the empty set is the singleton on the empty set. TODO: this generalizes rest0 21381 and could replace it. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ 𝑉 → (𝑋 ≠ ∅ → (𝑋 ↾t ∅) = {∅})) | ||
Theorem | bj-rest10b 33615 | Alternate version of bj-rest10 33614. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ (𝑉 ∖ {∅}) → (𝑋 ↾t ∅) = {∅}) | ||
Theorem | bj-restn0 33616 | An elementwise intersection on a nonempty family is nonempty. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑋 ≠ ∅ → (𝑋 ↾t 𝐴) ≠ ∅)) | ||
Theorem | bj-restn0b 33617 | Alternate version of bj-restn0 33616. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ (𝑉 ∖ {∅}) ∧ 𝐴 ∈ 𝑊) → (𝑋 ↾t 𝐴) ≠ ∅) | ||
Theorem | bj-restpw 33618 | The elementwise intersection on a powerset is the powerset of the intersection. This allows to prove for instance that the topology induced on a subset by the discrete topology is the discrete topology on that subset. See also restdis 21390 (which uses distop 21207 and restopn2 21389). (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝒫 𝑌 ↾t 𝐴) = 𝒫 (𝑌 ∩ 𝐴)) | ||
Theorem | bj-rest0 33619 | An elementwise intersection on a family containing the empty set contains the empty set. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∅ ∈ 𝑋 → ∅ ∈ (𝑋 ↾t 𝐴))) | ||
Theorem | bj-restb 33620 | An elementwise intersection by a set on a family containing a superset of that set contains that set. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ 𝑉 → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑋) → 𝐴 ∈ (𝑋 ↾t 𝐴))) | ||
Theorem | bj-restv 33621 | An elementwise intersection by a subset on a family containing the whole set contains the whole subset. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝐴 ⊆ ∪ 𝑋 ∧ ∪ 𝑋 ∈ 𝑋) → 𝐴 ∈ (𝑋 ↾t 𝐴)) | ||
Theorem | bj-resta 33622 | An elementwise intersection by a set on a family containing that set contains that set. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝑋 ∈ 𝑉 → (𝐴 ∈ 𝑋 → 𝐴 ∈ (𝑋 ↾t 𝐴))) | ||
Theorem | bj-restuni 33623 | The union of an elementwise intersection by a set is equal to the intersection with that set of the union of the family. See also restuni 21374 and restuni2 21379. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ∪ (𝑋 ↾t 𝐴) = (∪ 𝑋 ∩ 𝐴)) | ||
Theorem | bj-restuni2 33624 | The union of an elementwise intersection on a family of sets by a subset is equal to that subset. See also restuni 21374 and restuni2 21379. (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ ∪ 𝑋) → ∪ (𝑋 ↾t 𝐴) = 𝐴) | ||
Theorem | bj-restreg 33625 | A reformulation of the axiom of regularity using elementwise intersection. (RK: might have to be placed later since theorems in this section are to be moved early (in the section related to the algebra of sets).) (Contributed by BJ, 27-Apr-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → ∅ ∈ (𝐴 ↾t 𝐴)) | ||
Theorem | bj-intss 33626 | A nonempty intersection of a family of subsets of a class is included in that class. (Contributed by BJ, 7-Dec-2021.) |
⊢ (𝐴 ⊆ 𝒫 𝑋 → (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ 𝑋)) | ||
Theorem | bj-raldifsn 33627* | All elements in a set satisfy a given property if and only if all but one satisfy that property and that one also does. Typically, this can be used for characterizations that are proved using different methods for a given element and for all others, for instance zero and nonzero numbers, or the empty set and nonempty sets. (Contributed by BJ, 7-Dec-2021.) |
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐵 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝜑 ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ∧ 𝜓))) | ||
Theorem | bj-0int 33628* | If 𝐴 is a collection of subsets of 𝑋, like a topology, two equivalent ways to say that arbitrary intersections of elements of 𝐴 relative to 𝑋 belong to some class 𝐵 (in typical applications, 𝐴 itself). (Contributed by BJ, 7-Dec-2021.) |
⊢ (𝐴 ⊆ 𝒫 𝑋 → ((𝑋 ∈ 𝐵 ∧ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})∩ 𝑥 ∈ 𝐵) ↔ ∀𝑥 ∈ 𝒫 𝐴(𝑋 ∩ ∩ 𝑥) ∈ 𝐵)) | ||
Theorem | bj-mooreset 33629* |
A Moore collection is a set. That is, if we define a "Moore
class-predicate" by
(Moore𝐴 ↔ ∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥)
∈ 𝐴), then any
class satisfying that predicate is actually a set. Therefore, the
definition df-bj-moore 33631 is sufficient. Note that the closed sets of
a
topology form a Moore collection, so this remark also applies to
topologies and many other families of sets (namely, as soon as the whole
set is required to be a closed set, as can be seen from the proof, which
relies crucially on uniexr 7249).
Note: if, in the above predicate, we substitute 𝒫 𝑋 for 𝐴, then the last ∈ 𝒫 𝑋 could be weakened to ⊆ 𝑋, and then the predicate would be obviously satisfied since ∪ 𝒫 𝑋 = 𝑋 (unipw 5150) , making 𝒫 𝑋 a Moore collection in this weaker sense, even if 𝑋 is a proper class, but the addition of this single case does not add anything interesting. Instead, we have bj-discrmoore 33639. (Contributed by BJ, 8-Dec-2021.) |
⊢ (∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴 → 𝐴 ∈ V) | ||
Syntax | cmoore 33630 | Syntax for the class of Moore collections. |
class Moore | ||
Definition | df-bj-moore 33631* |
Define the class of Moore collections. This is to df-mre 16632 what
df-top 21106 is to df-topon 21123. For the sake of consistency, the function
defined at df-mre 16632 should be denoted by "MooreOn".
Note: df-mre 16632 singles out the empty intersection. This is not necessary. It could be written instead Moore = (𝑥 ∈ V ↦ {𝑦 ∈ 𝒫 𝒫 𝑥 ∣ ∀𝑧 ∈ 𝒫 𝑦(𝑥 ∩ ∩ 𝑧) ∈ 𝑦}) and the equivalence of both definitions is proved by bj-0int 33628. There is no added generality in defining a "Moore predicate" for arbitrary classes, since a Moore class satisfying such a predicate is automatically a set (see bj-mooreset 33629). (Contributed by BJ, 27-Apr-2021.) |
⊢ Moore = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 ∩ ∩ 𝑦) ∈ 𝑥} | ||
Theorem | bj-ismoore 33632* | Characterization of Moore collections among sets. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Moore ↔ ∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴)) | ||
Theorem | bj-ismoorec 33633* | Characterization of Moore collections. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝐴 ∈ Moore ↔ (𝐴 ∈ V ∧ ∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴)) | ||
Theorem | bj-ismoored0 33634 | Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝐴 ∈ Moore → ∪ 𝐴 ∈ 𝐴) | ||
Theorem | bj-ismoored 33635 | Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝜑 → 𝐴 ∈ Moore) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (∪ 𝐴 ∩ ∩ 𝐵) ∈ 𝐴) | ||
Theorem | bj-ismoored2 33636 | Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝜑 → 𝐴 ∈ Moore) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐵 ≠ ∅) ⇒ ⊢ (𝜑 → ∩ 𝐵 ∈ 𝐴) | ||
Theorem | bj-ismooredr 33637* | Sufficient condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ∈ Moore) | ||
Theorem | bj-ismooredr2 33638* | Sufficient condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ∪ 𝐴 ∈ 𝐴) & ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ∩ 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ∈ Moore) | ||
Theorem | bj-discrmoore 33639 | The discrete Moore collection on a set. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ Moore) | ||
Theorem | bj-0nmoore 33640 | The empty set is not a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ ¬ ∅ ∈ Moore | ||
Theorem | bj-snmoore 33641 | A singleton is a Moore collection. (Contributed by BJ, 9-Dec-2021.) |
⊢ (𝐴 ∈ V ↔ {𝐴} ∈ Moore) | ||
Theorem | bj-0nelmpt 33642 | The empty set is not an element of a function (given in maps-to notation). (Contributed by BJ, 30-Dec-2020.) |
⊢ ¬ ∅ ∈ (𝑥 ∈ 𝐴 ↦ 𝐵) | ||
Theorem | bj-mptval 33643 | Value of a function given in maps-to notation. (Contributed by BJ, 30-Dec-2020.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑋 ∈ 𝐴 → (((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑋) = 𝑌 ↔ 𝑋(𝑥 ∈ 𝐴 ↦ 𝐵)𝑌))) | ||
Theorem | bj-dfmpt2a 33644* | An equivalent definition of df-mpt2 6927. (Contributed by BJ, 30-Dec-2020.) |
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈𝑠, 𝑡〉 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑠 = 〈𝑥, 𝑦〉 ∧ 𝑡 = 𝐶)} | ||
Theorem | bj-mpt2mptALT 33645* | Alternate proof of mpt2mpt 7029. (Contributed by BJ, 30-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) ⇒ ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) | ||
Syntax | cmpt3 33646 | Extend the definition of a class to include maps-to notation for functions with three arguments. |
class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷) | ||
Definition | df-bj-mpt3 33647* | Define maps-to notation for functions with three arguments. See df-mpt 4966 and df-mpt2 6927 for functions with one and two arguments respectively. This definition is analogous to bj-dfmpt2a 33644. (Contributed by BJ, 11-Apr-2020.) |
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵, 𝑧 ∈ 𝐶 ↦ 𝐷) = {〈𝑠, 𝑡〉 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝑠 = 〈𝑥, 𝑦, 𝑧〉 ∧ 𝑡 = 𝐷)} | ||
Currying and uncurrying. See also df-cur and df-unc 7676. Contrary to these, the definitions in this section are parameterized. | ||
Syntax | csethom 33648 | Syntax for the set of set morphisms. |
class Set⟶ | ||
Definition | df-bj-sethom 33649* |
Define the set of functions (morphisms of sets) between two sets. Same
as df-map 8142 with arguments swapped. TODO: prove the same
staple lemmas
as for ↑𝑚.
Remark: one may define Set⟶ = (𝑥 ∈ dom Struct , 𝑦 ∈ dom Struct ↦ {𝑓 ∣ 𝑓:(Base‘𝑥)⟶(Base‘𝑦)}) so that for morphisms between other structures, one could write ... = {𝑓 ∈ (𝑥 Set⟶ 𝑦) ∣ ...}. (Contributed by BJ, 11-Apr-2020.) |
⊢ Set⟶ = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑥⟶𝑦}) | ||
Syntax | ctophom 33650 | Syntax for the set of topological morphisms. |
class Top⟶ | ||
Definition | df-bj-tophom 33651* | Define the set of continuous functions (morphisms of topological spaces) between two topological spaces. Similar to df-cn 21439 (which is in terms of topologies instead of topological spaces). (Contributed by BJ, 10-Feb-2022.) |
⊢ Top⟶ = (𝑥 ∈ TopSp, 𝑦 ∈ TopSp ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (TopOpen‘𝑦)(◡𝑓 “ 𝑢) ∈ (TopOpen‘𝑥)}) | ||
Syntax | cmgmhom 33652 | Syntax for the set of magma morphisms. |
class Mgm⟶ | ||
Definition | df-bj-mgmhom 33653* | Define the set of magma morphisms between two magmas. If domain and codomain are semigroups, monoids, or groups, then one obtains the set of morphisms of these structures. (Contributed by BJ, 10-Feb-2022.) |
⊢ Mgm⟶ = (𝑥 ∈ Mgm, 𝑦 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))}) | ||
Syntax | ctopmgmhom 33654 | Syntax for the set of topological magma morphisms. |
class TopMgm⟶ | ||
Definition | df-bj-topmgmhom 33655* | Define the set of topological magma morphisms (continuous magma morphisms) between two topological magmas. If domain and codomain are topological semigroups, monoids, or groups, then one obtains the set of morphisms of these structures. This definition is currently stated with topological monoid domain and codomain, since topological magmas are currently not defined in set.mm. (Contributed by BJ, 10-Feb-2022.) |
⊢ TopMgm⟶ = (𝑥 ∈ TopMnd, 𝑦 ∈ TopMnd ↦ ((𝑥 Top⟶ 𝑦) ∩ (𝑥 Mgm⟶ 𝑦))) | ||
Syntax | ccur- 33656 | Syntax for the parameterized currying function. |
class curry_ | ||
Definition | df-bj-cur 33657* | Define currying. See also df-cur 7675. (Contributed by BJ, 11-Apr-2020.) |
⊢ curry_ = (𝑥 ∈ V, 𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑓 ∈ ((𝑥 × 𝑦) Set⟶ 𝑧) ↦ (𝑎 ∈ 𝑥 ↦ (𝑏 ∈ 𝑦 ↦ (𝑓‘〈𝑎, 𝑏〉))))) | ||
Syntax | cunc- 33658 | Notation for the parameterized uncurrying function. |
class uncurry_ | ||
Definition | df-bj-unc 33659* | Define uncurrying. See also df-unc 7676. (Contributed by BJ, 11-Apr-2020.) |
⊢ uncurry_ = (𝑥 ∈ V, 𝑦 ∈ V, 𝑧 ∈ V ↦ (𝑓 ∈ (𝑥 Set⟶ (𝑦 Set⟶ 𝑧)) ↦ (𝑎 ∈ 𝑥, 𝑏 ∈ 𝑦 ↦ ((𝑓‘𝑎)‘𝑏)))) | ||
Groundwork for changing the definition, syntax and token for component-setting in extensible structures. See https://github.com/metamath/set.mm/issues/2401 | ||
Syntax | cstrset 33660 | Syntax for component-setting in extensible structures. |
class [𝐵 / 𝐴]struct𝑆 | ||
Definition | df-strset 33661 | Component-setting in extensible structures. Define the extensible structure [𝐵 / 𝐴]struct𝑆, which is like the extensible structure 𝑆 except that the value 𝐵 has been put in the slot 𝐴 (replacing the current value if there was already one). In such expressions, 𝐴 is generally substituted for slot mnemonics like Base or +g or dist. (Contributed by BJ, 13-Feb-2022.) |
⊢ [𝐵 / 𝐴]struct𝑆 = ((𝑆 ↾ (V ∖ {(𝐴‘ndx)})) ∪ {〈(𝐴‘ndx), 𝐵〉}) | ||
Theorem | setsstrset 33662 | Relation between df-sets 16262 and df-strset 33661. Temporary theorem kept during the transition from the former to the latter. (Contributed by BJ, 13-Feb-2022.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → [𝐵 / 𝐴]struct𝑆 = (𝑆 sSet 〈(𝐴‘ndx), 𝐵〉)) | ||
In this section, we indroduce several supersets of the set ℝ of real numbers and the set ℂ of complex numbers. Once they are given their usual topologies, which are locally compact, both topological spaces have a one-point compactification. They are denoted by ℝ̂ and ℂ̂ respectively, defined in df-bj-cchat 33710 and df-bj-rrhat 33712, and the point at infinity is denoted by ∞, defined in df-bj-infty 33708. Both ℝ and ℂ also have "directional compactifications", denoted respectively by ℝ̅, defined in df-bj-rrbar 33706 (already defined as ℝ*, see df-xr 10415) and ℂ̅, defined in df-bj-ccbar 33693. Since ℂ̅ does not seem to be standard, we describe it in some detail. It is obtained by adding to ℂ a "point at infinity at the end of each ray with origin at 0". Although ℂ̅ is not an important object in itself, the motivation for introducing it is to provide a common superset to both ℝ̅ and ℂ and to define algebraic operations (addition, opposite, multiplication, inverse) as widely as reasonably possible. Mathematically, ℂ̅ is the quotient of ((ℂ × ℝ≥0) ∖ {〈0, 0〉}) by the diagonal multiplicative action of ℝ>0 (think of the closed "northern hemisphere" in ℝ^3 identified with (ℂ × ℝ), that each open ray from 0 included in the closed northern half-space intersects exactly once). Since in set.mm, we want to have a genuine inclusion ℂ ⊆ ℂ̅, we instead define ℂ̅ as the (disjoint) union of ℂ with a circle at infinity denoted by ℂ∞. To have a genuine inclusion ℝ̅ ⊆ ℂ̅, we define +∞ and -∞ as certain points in ℂ∞. Thanks to this framework, one has the genuine inclusions ℝ ⊆ ℝ̅ and ℝ ⊆ ℝ̂ and similarly ℂ ⊆ ℂ̅ and ℂ ⊆ ℂ̂. Furthermore, one has ℝ ⊆ ℂ as well as ℝ̅ ⊆ ℂ̅ and ℝ̂ ⊆ ℂ̂. Furthermore, we define the main algebraic operations on (ℂ̅ ∪ ℂ̂), which is not very mathematical, but "overloads" the operations, so that one can use the same notation in all cases. | ||
Complements on the identity relation. | ||
Theorem | bj-elid 33663 | Characterization of the elements of I. (Contributed by BJ, 22-Jun-2019.) |
⊢ (𝐴 ∈ I ↔ (𝐴 ∈ (V × V) ∧ (1st ‘𝐴) = (2nd ‘𝐴))) | ||
Theorem | bj-elid2 33664 | Characterization of the elements of I. (Contributed by BJ, 22-Jun-2019.) |
⊢ (𝐴 ∈ (𝑉 × 𝑊) → (𝐴 ∈ I ↔ (1st ‘𝐴) = (2nd ‘𝐴))) | ||
Theorem | bj-elid3 33665 | Characterization of the couples in I. (Contributed by BJ, 29-Mar-2020.) |
⊢ (〈𝐴, 𝐵〉 ∈ I ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵)) | ||
Theorem | bj-elid4 33666 | Characterization of the couples in I whose first component is a setvar. (Contributed by BJ, 29-Mar-2020.) |
⊢ (〈𝑥, 𝐴〉 ∈ I ↔ 𝑥 = 𝐴) | ||
Definition of the diagonal in the Cartesian square of a set. | ||
Syntax | cdiag2 33667 | Syntax for the diagonal of the Cartesian square of a set. |
class Diag | ||
Definition | df-bj-diag 33668 | Define the diagonal of the Cartesian square of a set. (Contributed by BJ, 22-Jun-2019.) |
⊢ Diag = (𝑥 ∈ V ↦ ( I ∩ (𝑥 × 𝑥))) | ||
Theorem | bj-diagval 33669 | Value of the diagonal. (Contributed by BJ, 22-Jun-2019.) |
⊢ (𝐴 ∈ 𝑉 → (Diag‘𝐴) = ( I ∩ (𝐴 × 𝐴))) | ||
Theorem | bj-eldiag 33670 | Characterization of the elements of the diagonal of a Cartesian square. (Contributed by BJ, 22-Jun-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ (Diag‘𝐴) ↔ (𝐵 ∈ (𝐴 × 𝐴) ∧ (1st ‘𝐵) = (2nd ‘𝐵)))) | ||
Theorem | bj-eldiag2 33671 | Characterization of the elements of the diagonal of a Cartesian square. (Contributed by BJ, 22-Jun-2019.) |
⊢ (𝐴 ∈ 𝑉 → (〈𝐵, 𝐶〉 ∈ (Diag‘𝐴) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 = 𝐶))) | ||
We parameterize the set of infinite extended complex numbers ℂ∞ (df-bj-ccinfty 33689) using the reals (df-r 10282) via the function +∞eiτ. Since at that point, we have only defined the set of reals but no operations on it, we define a temporary "fractional part" function, which is more convenient to define on the temporary reals (df-nr 10213) since we use operations on the latter. We also define a temporary "one-half" in order to define minus infinity (df-bj-minfty 33701) and then we can define the sets of extended real and complex numbers and the projective real and complex line, as well as addition and negation and also the order on the extended reals (which bypasses the intermediate definition of a temporary order on the reals and then a superseding one on the extended reals). | ||
Syntax | cfractemp 33672 | Syntax for the fractional part of a tempopary real. |
class {R | ||
Definition | df-bj-fractemp 33673* |
Temporary definition: fractional part of a temporary real.
To understand this definition, recall the canonical injection ω⟶R, 𝑛 ↦ [{𝑥 ∈ Q ∣ 𝑥 <Q 〈suc 𝑛, 1o〉}, 1P] ~R where we successively take the successor of 𝑛 to land in positive integers, then take the couple with 1o as second component to land in positive rationals, then take the Dedekind cut that positive rational forms, and finally take the equivalence class of the couple with 1P as second component. Adding one at the beginning and subtracting it at the end is necessary since the constructions used in set.mm use the positive integers, positive rationals, and positive reals as intermediate number systems. (Contributed by BJ, 22-Jan-2023.) The precise definition is irrelevant and should generally not be used. One could even inline it. The definitive fractional part of an extended or projective complex number will be defined later. (New usage is discouraged.) |
⊢ {R = (𝑥 ∈ R ↦ (℩𝑦 ∈ R ((𝑦 = 0R ∨ (0R <R 𝑦 ∧ 𝑦 <R 1R)) ∧ ∃𝑛 ∈ ω ([〈{𝑧 ∈ Q ∣ 𝑧 <Q 〈suc 𝑛, 1o〉}, 1P〉] ~R +R 𝑦) = 𝑥))) | ||
Syntax | cinftyexpitau 33674 | Syntax for the function +∞eiτ parameterizing ℂ∞. |
class +∞eiτ | ||
Definition | df-bj-inftyexpitau 33675 | Definition of the auxiliary function +∞eiτ parameterizing the circle at infinity ℂ∞ in ℂ̅. We use coupling with {R} to simplify the proof of bj-inftyexpitaudisj 33682. (Contributed by BJ, 22-Jan-2023.) The precise definition is irrelevant and should generally not be used. TODO: prove only the necessary lemmas to prove ⊢ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((+∞eiτ‘𝐴) = (+∞eiτ‘𝐵) ↔ (𝐴 − 𝐵) ∈ ℤ)). (New usage is discouraged.) |
⊢ +∞eiτ = (𝑥 ∈ ℝ ↦ 〈({R‘(1st ‘𝑥)), {R}〉) | ||
Syntax | cccinftyN 33676 | Syntax for the circle at infinity ℂ∞N. |
class ℂ∞N | ||
Definition | df-bj-ccinftyN 33677 | Definition of the circle at infinity ℂ∞N. (Contributed by BJ, 22-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.) |
⊢ ℂ∞N = ran +∞eiτ | ||
Theorem | bj-inftyexpitaufo 33678 | The function +∞eiτ written as a surjection with domain and range. (Contributed by BJ, 4-Feb-2023.) |
⊢ +∞eiτ:ℝ–onto→ℂ∞N | ||
Syntax | chalf 33679 | Syntax for the temporary one-half. |
class 1/2 | ||
Definition | df-bj-onehalf 33680 | Define temporarily the real number "one-half". (Contributed by BJ, 4-Feb-2023.) Once the machinery is developed, the number "one-half" can be denoted by (1 / 2). (New usage is discouraged.) |
⊢ 1/2 = 〈(℩𝑥 ∈ R (𝑥 +R 𝑥) = 1R), 0R〉 | ||
Theorem | bj-nsnid 33681 | A set does not contain the singleton formed on it. More precisely, one can prove that a class contains the singleton formed on it if and only if it is proper and contains the "singleton formed on it", which is the empty set: ⊢ ¬ ({𝐴} ∈ 𝐴 ↔ (∅ ∈ 𝐴 → 𝐴 ∈ V)). (Contributed by BJ, 4-Feb-2023.) |
⊢ (𝐴 ∈ 𝑉 → ¬ {𝐴} ∈ 𝐴) | ||
Theorem | bj-inftyexpitaudisj 33682 | An element of the circle at infinity is not a complex number. (Contributed by BJ, 4-Feb-2023.) |
⊢ ¬ (+∞eiτ‘𝐴) ∈ ℂ | ||
Syntax | cinftyexpi 33683 | Syntax for the function +∞ei parameterizing ℂ∞. |
class +∞ei | ||
Definition | df-bj-inftyexpi 33684 | Definition of the auxiliary function +∞ei parameterizing the circle at infinity ℂ∞ in ℂ̅. We use coupling with ℂ to simplify the proof of bj-ccinftydisj 33690. It could seem more natural to define +∞ei on all of ℝ, but we want to use only basic functions in the definition of ℂ̅. TODO: transition to df-bj-inftyexpitau 33675 instead. (Contributed by BJ, 22-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.) |
⊢ +∞ei = (𝑥 ∈ (-π(,]π) ↦ 〈𝑥, ℂ〉) | ||
Theorem | bj-inftyexpiinv 33685 | Utility theorem for the inverse of +∞ei. (Contributed by BJ, 22-Jun-2019.) This utility theorem is irrelevant and should generally not be used. (New usage is discouraged.) |
⊢ (𝐴 ∈ (-π(,]π) → (1st ‘(+∞ei‘𝐴)) = 𝐴) | ||
Theorem | bj-inftyexpiinj 33686 | Injectivity of the parameterization +∞ei. Remark: a more conceptual proof would use bj-inftyexpiinv 33685 and the fact that a function with a retraction is injective. (Contributed by BJ, 22-Jun-2019.) |
⊢ ((𝐴 ∈ (-π(,]π) ∧ 𝐵 ∈ (-π(,]π)) → (𝐴 = 𝐵 ↔ (+∞ei‘𝐴) = (+∞ei‘𝐵))) | ||
Theorem | bj-inftyexpidisj 33687 | An element of the circle at infinity is not a complex number. (Contributed by BJ, 22-Jun-2019.) This utility theorem is irrelevant and should generally not be used. (New usage is discouraged.) |
⊢ ¬ (+∞ei‘𝐴) ∈ ℂ | ||
Syntax | cccinfty 33688 | Syntax for the circle at infinity ℂ∞. |
class ℂ∞ | ||
Definition | df-bj-ccinfty 33689 | Definition of the circle at infinity ℂ∞. (Contributed by BJ, 22-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.) |
⊢ ℂ∞ = ran +∞ei | ||
Theorem | bj-ccinftydisj 33690 | The circle at infinity is disjoint from the set of complex numbers. (Contributed by BJ, 22-Jun-2019.) |
⊢ (ℂ ∩ ℂ∞) = ∅ | ||
Theorem | bj-elccinfty 33691 | A lemma for infinite extended complex numbers. (Contributed by BJ, 27-Jun-2019.) |
⊢ (𝐴 ∈ (-π(,]π) → (+∞ei‘𝐴) ∈ ℂ∞) | ||
Syntax | cccbar 33692 | Syntax for the set of extended complex numbers ℂ̅. |
class ℂ̅ | ||
Definition | df-bj-ccbar 33693 | Definition of the set of extended complex numbers ℂ̅. (Contributed by BJ, 22-Jun-2019.) |
⊢ ℂ̅ = (ℂ ∪ ℂ∞) | ||
Theorem | bj-ccssccbar 33694 | Complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.) |
⊢ ℂ ⊆ ℂ̅ | ||
Theorem | bj-ccinftyssccbar 33695 | Infinite extended complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019.) |
⊢ ℂ∞ ⊆ ℂ̅ | ||
Syntax | cpinfty 33696 | Syntax for "plus infinity". |
class +∞ | ||
Definition | df-bj-pinfty 33697 | Definition of "plus infinity". (Contributed by BJ, 27-Jun-2019.) |
⊢ +∞ = (+∞ei‘0) | ||
Theorem | bj-pinftyccb 33698 | The class +∞ is an extended complex number. (Contributed by BJ, 27-Jun-2019.) |
⊢ +∞ ∈ ℂ̅ | ||
Theorem | bj-pinftynrr 33699 | The extended complex number +∞ is not a complex number. (Contributed by BJ, 27-Jun-2019.) |
⊢ ¬ +∞ ∈ ℂ | ||
Syntax | cminfty 33700 | Syntax for "minus infinity". |
class -∞ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |