![]() |
Intuitionistic Logic Explorer Theorem List (p. 137 of 150) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cnfldmul 13601 | The multiplication operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) |
⊢ · = (.r‘ℂfld) | ||
Theorem | cnfldcj 13602 | The conjugation operation of the field of complex numbers. (Contributed by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by Thierry Arnoux, 17-Dec-2017.) |
⊢ ∗ = (*𝑟‘ℂfld) | ||
Theorem | cncrng 13603 | The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.) |
⊢ ℂfld ∈ CRing | ||
Theorem | cnring 13604 | The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ ℂfld ∈ Ring | ||
Theorem | cnfld0 13605 | Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 0 = (0g‘ℂfld) | ||
Theorem | cnfld1 13606 | One is the unity element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ 1 = (1r‘ℂfld) | ||
Theorem | cnfldneg 13607 | The additive inverse in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
⊢ (𝑋 ∈ ℂ → ((invg‘ℂfld)‘𝑋) = -𝑋) | ||
Theorem | cnfldplusf 13608 | The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ + = (+𝑓‘ℂfld) | ||
Theorem | cnfldsub 13609 | The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ − = (-g‘ℂfld) | ||
Theorem | cnfldmulg 13610 | The group multiple function in the field of complex numbers. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℂ) → (𝐴(.g‘ℂfld)𝐵) = (𝐴 · 𝐵)) | ||
Theorem | cnfldexp 13611 | The exponentiation operator in the field of complex numbers (for nonnegative exponents). (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ0) → (𝐵(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑𝐵)) | ||
Theorem | cnsubmlem 13612* | Lemma for nn0subm 13617 and friends. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ 0 ∈ 𝐴 ⇒ ⊢ 𝐴 ∈ (SubMnd‘ℂfld) | ||
Theorem | cnsubglem 13613* | Lemma for cnsubrglem 13614 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 𝐵 ∈ 𝐴 ⇒ ⊢ 𝐴 ∈ (SubGrp‘ℂfld) | ||
Theorem | cnsubrglem 13614* | Lemma for zsubrg 13615 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 + 𝑦) ∈ 𝐴) & ⊢ (𝑥 ∈ 𝐴 → -𝑥 ∈ 𝐴) & ⊢ 1 ∈ 𝐴 & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴) ⇒ ⊢ 𝐴 ∈ (SubRing‘ℂfld) | ||
Theorem | zsubrg 13615 | The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ ℤ ∈ (SubRing‘ℂfld) | ||
Theorem | gzsubrg 13616 | The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
⊢ ℤ[i] ∈ (SubRing‘ℂfld) | ||
Theorem | nn0subm 13617 | The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ ℕ0 ∈ (SubMnd‘ℂfld) | ||
Theorem | rege0subm 13618 | The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ (0[,)+∞) ∈ (SubMnd‘ℂfld) | ||
Theorem | zsssubrg 13619 | The integers are a subset of any subring of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝑅 ∈ (SubRing‘ℂfld) → ℤ ⊆ 𝑅) | ||
According to Wikipedia ("Integer", 25-May-2019, https://en.wikipedia.org/wiki/Integer) "The integers form a unital ring which is the most basic one, in the following sense: for any unital ring, there is a unique ring homomorphism from the integers into this ring. This universal property, namely to be an initial object in the category of [unital] rings, characterizes the ring 𝑍." In set.mm, there was no explicit definition for the ring of integers until June 2019, but it was denoted by (ℂfld ↾s ℤ), the field of complex numbers restricted to the integers. In zringring 13623 it is shown that this restriction is a ring, and zringbas 13626 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as Definition df-zring 13621 of the ring of integers. Remark: Instead of using the symbol "ZZrng" analogous to ℂfld used for the field of complex numbers, we have chosen the version with an "i" to indicate that the ring of integers is a unital ring, see also Wikipedia ("Rng (algebra)", 9-Jun-2019, https://en.wikipedia.org/wiki/Rng_(algebra) 13621). | ||
Syntax | czring 13620 | Extend class notation with the (unital) ring of integers. |
class ℤring | ||
Definition | df-zring 13621 | The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.) |
⊢ ℤring = (ℂfld ↾s ℤ) | ||
Theorem | zringcrng 13622 | The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.) |
⊢ ℤring ∈ CRing | ||
Theorem | zringring 13623 | The ring of integers is a ring. (Contributed by AV, 20-May-2019.) (Revised by AV, 9-Jun-2019.) (Proof shortened by AV, 13-Jun-2019.) |
⊢ ℤring ∈ Ring | ||
Theorem | zringabl 13624 | The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.) |
⊢ ℤring ∈ Abel | ||
Theorem | zringgrp 13625 | The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.) |
⊢ ℤring ∈ Grp | ||
Theorem | zringbas 13626 | The integers are the base of the ring of integers. (Contributed by Thierry Arnoux, 31-Oct-2017.) (Revised by AV, 9-Jun-2019.) |
⊢ ℤ = (Base‘ℤring) | ||
Theorem | zringplusg 13627 | The addition operation of the ring of integers. (Contributed by Thierry Arnoux, 8-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
⊢ + = (+g‘ℤring) | ||
Theorem | zringmulg 13628 | The multiplication (group power) operation of the group of integers. (Contributed by Thierry Arnoux, 31-Oct-2017.) (Revised by AV, 9-Jun-2019.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴(.g‘ℤring)𝐵) = (𝐴 · 𝐵)) | ||
Theorem | zringmulr 13629 | The multiplication operation of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
⊢ · = (.r‘ℤring) | ||
Theorem | zring0 13630 | The zero element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
⊢ 0 = (0g‘ℤring) | ||
Theorem | zring1 13631 | The unity element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
⊢ 1 = (1r‘ℤring) | ||
Theorem | zringnzr 13632 | The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.) |
⊢ ℤring ∈ NzRing | ||
Theorem | dvdsrzring 13633 | Ring divisibility in the ring of integers corresponds to ordinary divisibility in ℤ. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.) |
⊢ ∥ = (∥r‘ℤring) | ||
Theorem | zringinvg 13634 | The additive inverse of an element of the ring of integers. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
⊢ (𝐴 ∈ ℤ → -𝐴 = ((invg‘ℤring)‘𝐴)) | ||
Theorem | zringsubgval 13635 | Subtraction in the ring of integers. (Contributed by AV, 3-Aug-2019.) |
⊢ − = (-g‘ℤring) ⇒ ⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑋 − 𝑌) = (𝑋 − 𝑌)) | ||
Theorem | zringmpg 13636 | The multiplicative group of the ring of integers is the restriction of the multiplicative group of the complex numbers to the integers. (Contributed by AV, 15-Jun-2019.) |
⊢ ((mulGrp‘ℂfld) ↾s ℤ) = (mulGrp‘ℤring) | ||
A topology on a set is a set of subsets of that set, called open sets, which satisfy certain conditions. One condition is that the whole set be an open set. Therefore, a set is recoverable from a topology on it (as its union), and it may sometimes be more convenient to consider topologies without reference to the underlying set. | ||
Syntax | ctop 13637 | Syntax for the class of topologies. |
class Top | ||
Definition | df-top 13638* |
Define the class of topologies. It is a proper class. See istopg 13639 and
istopfin 13640 for the corresponding characterizations,
using respectively
binary intersections like in this definition and nonempty finite
intersections.
The final form of the definition is due to Bourbaki (Def. 1 of [BourbakiTop1] p. I.1), while the idea of defining a topology in terms of its open sets is due to Aleksandrov. For the convoluted history of the definitions of these notions, see Gregory H. Moore, The emergence of open sets, closed sets, and limit points in analysis and topology, Historia Mathematica 35 (2008) 220--241. (Contributed by NM, 3-Mar-2006.) (Revised by BJ, 20-Oct-2018.) |
⊢ Top = {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)} | ||
Theorem | istopg 13639* |
Express the predicate "𝐽 is a topology". See istopfin 13640 for
another characterization using nonempty finite intersections instead of
binary intersections.
Note: In the literature, a topology is often represented by a calligraphic letter T, which resembles the letter J. This confusion may have led to J being used by some authors (e.g., K. D. Joshi, Introduction to General Topology (1983), p. 114) and it is convenient for us since we later use 𝑇 to represent linear transformations (operators). (Contributed by Stefan Allan, 3-Mar-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ (𝐽 ∈ 𝐴 → (𝐽 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽))) | ||
Theorem | istopfin 13640* | Express the predicate "𝐽 is a topology" using nonempty finite intersections instead of binary intersections as in istopg 13639. It is not clear we can prove the converse without adding additional conditions. (Contributed by NM, 19-Jul-2006.) (Revised by Jim Kingdon, 14-Jan-2023.) |
⊢ (𝐽 ∈ Top → (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥((𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐽))) | ||
Theorem | uniopn 13641 | The union of a subset of a topology (that is, the union of any family of open sets of a topology) is an open set. (Contributed by Stefan Allan, 27-Feb-2006.) |
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽) → ∪ 𝐴 ∈ 𝐽) | ||
Theorem | iunopn 13642* | The indexed union of a subset of a topology is an open set. (Contributed by NM, 5-Oct-2006.) |
⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽) | ||
Theorem | inopn 13643 | The intersection of two open sets of a topology is an open set. (Contributed by NM, 17-Jul-2006.) |
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽) | ||
Theorem | fiinopn 13644 | The intersection of a nonempty finite family of open sets is open. (Contributed by FL, 20-Apr-2012.) |
⊢ (𝐽 ∈ Top → ((𝐴 ⊆ 𝐽 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → ∩ 𝐴 ∈ 𝐽)) | ||
Theorem | unopn 13645 | The union of two open sets is open. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∪ 𝐵) ∈ 𝐽) | ||
Theorem | 0opn 13646 | The empty set is an open subset of any topology. (Contributed by Stefan Allan, 27-Feb-2006.) |
⊢ (𝐽 ∈ Top → ∅ ∈ 𝐽) | ||
Theorem | 0ntop 13647 | The empty set is not a topology. (Contributed by FL, 1-Jun-2008.) |
⊢ ¬ ∅ ∈ Top | ||
Theorem | topopn 13648 | The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) | ||
Theorem | eltopss 13649 | A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋) | ||
Syntax | ctopon 13650 | Syntax for the function of topologies on sets. |
class TopOn | ||
Definition | df-topon 13651* | Define the function that associates with a set the set of topologies on it. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ TopOn = (𝑏 ∈ V ↦ {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗}) | ||
Theorem | funtopon 13652 | The class TopOn is a function. (Contributed by BJ, 29-Apr-2021.) |
⊢ Fun TopOn | ||
Theorem | istopon 13653 | Property of being a topology with a given base set. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽)) | ||
Theorem | topontop 13654 | A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top) | ||
Theorem | toponuni 13655 | The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽) | ||
Theorem | topontopi 13656 | A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐽 ∈ (TopOn‘𝐵) ⇒ ⊢ 𝐽 ∈ Top | ||
Theorem | toponunii 13657 | The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐽 ∈ (TopOn‘𝐵) ⇒ ⊢ 𝐵 = ∪ 𝐽 | ||
Theorem | toptopon 13658 | Alternative definition of Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) | ||
Theorem | toptopon2 13659 | A topology is the same thing as a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) | ||
Theorem | topontopon 13660 | A topology on a set is a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ (TopOn‘∪ 𝐽)) | ||
Theorem | toponrestid 13661 | Given a topology on a set, restricting it to that same set has no effect. (Contributed by Jim Kingdon, 6-Jul-2022.) |
⊢ 𝐴 ∈ (TopOn‘𝐵) ⇒ ⊢ 𝐴 = (𝐴 ↾t 𝐵) | ||
Theorem | toponsspwpwg 13662 | The set of topologies on a set is included in the double power set of that set. (Contributed by BJ, 29-Apr-2021.) (Revised by Jim Kingdon, 16-Jan-2023.) |
⊢ (𝐴 ∈ 𝑉 → (TopOn‘𝐴) ⊆ 𝒫 𝒫 𝐴) | ||
Theorem | dmtopon 13663 | The domain of TopOn is V. (Contributed by BJ, 29-Apr-2021.) |
⊢ dom TopOn = V | ||
Theorem | fntopon 13664 | The class TopOn is a function with domain V. (Contributed by BJ, 29-Apr-2021.) |
⊢ TopOn Fn V | ||
Theorem | toponmax 13665 | The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽) | ||
Theorem | toponss 13666 | A member of a topology is a subset of its underlying set. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋) | ||
Theorem | toponcom 13667 | If 𝐾 is a topology on the base set of topology 𝐽, then 𝐽 is a topology on the base of 𝐾. (Contributed by Mario Carneiro, 22-Aug-2015.) |
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ (TopOn‘∪ 𝐽)) → 𝐽 ∈ (TopOn‘∪ 𝐾)) | ||
Theorem | toponcomb 13668 | Biconditional form of toponcom 13667. (Contributed by BJ, 5-Dec-2021.) |
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 ∈ (TopOn‘∪ 𝐾) ↔ 𝐾 ∈ (TopOn‘∪ 𝐽))) | ||
Theorem | topgele 13669 | The topologies over the same set have the greatest element (the discrete topology) and the least element (the indiscrete topology). (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 16-Sep-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → ({∅, 𝑋} ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 𝑋)) | ||
Syntax | ctps 13670 | Syntax for the class of topological spaces. |
class TopSp | ||
Definition | df-topsp 13671 | Define the class of topological spaces (as extensible structures). (Contributed by Stefan O'Rear, 13-Aug-2015.) |
⊢ TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))} | ||
Theorem | istps 13672 | Express the predicate "is a topological space". (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐴 = (Base‘𝐾) & ⊢ 𝐽 = (TopOpen‘𝐾) ⇒ ⊢ (𝐾 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐴)) | ||
Theorem | istps2 13673 | Express the predicate "is a topological space". (Contributed by NM, 20-Oct-2012.) |
⊢ 𝐴 = (Base‘𝐾) & ⊢ 𝐽 = (TopOpen‘𝐾) ⇒ ⊢ (𝐾 ∈ TopSp ↔ (𝐽 ∈ Top ∧ 𝐴 = ∪ 𝐽)) | ||
Theorem | tpsuni 13674 | The base set of a topological space. (Contributed by FL, 27-Jun-2014.) |
⊢ 𝐴 = (Base‘𝐾) & ⊢ 𝐽 = (TopOpen‘𝐾) ⇒ ⊢ (𝐾 ∈ TopSp → 𝐴 = ∪ 𝐽) | ||
Theorem | tpstop 13675 | The topology extractor on a topological space is a topology. (Contributed by FL, 27-Jun-2014.) |
⊢ 𝐽 = (TopOpen‘𝐾) ⇒ ⊢ (𝐾 ∈ TopSp → 𝐽 ∈ Top) | ||
Theorem | tpspropd 13676 | A topological space depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿)) ⇒ ⊢ (𝜑 → (𝐾 ∈ TopSp ↔ 𝐿 ∈ TopSp)) | ||
Theorem | topontopn 13677 | Express the predicate "is a topological space". (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐴 = (Base‘𝐾) & ⊢ 𝐽 = (TopSet‘𝐾) ⇒ ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐽 = (TopOpen‘𝐾)) | ||
Theorem | tsettps 13678 | If the topology component is already correctly truncated, then it forms a topological space (with the topology extractor function coming out the same as the component). (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐴 = (Base‘𝐾) & ⊢ 𝐽 = (TopSet‘𝐾) ⇒ ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ TopSp) | ||
Theorem | istpsi 13679 | Properties that determine a topological space. (Contributed by NM, 20-Oct-2012.) |
⊢ (Base‘𝐾) = 𝐴 & ⊢ (TopOpen‘𝐾) = 𝐽 & ⊢ 𝐴 = ∪ 𝐽 & ⊢ 𝐽 ∈ Top ⇒ ⊢ 𝐾 ∈ TopSp | ||
Theorem | eltpsg 13680 | Properties that determine a topological space from a construction (using no explicit indices). (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐾 = {〈(Base‘ndx), 𝐴〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ TopSp) | ||
Theorem | eltpsi 13681 | Properties that determine a topological space from a construction (using no explicit indices). (Contributed by NM, 20-Oct-2012.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐾 = {〈(Base‘ndx), 𝐴〉, 〈(TopSet‘ndx), 𝐽〉} & ⊢ 𝐴 = ∪ 𝐽 & ⊢ 𝐽 ∈ Top ⇒ ⊢ 𝐾 ∈ TopSp | ||
Syntax | ctb 13682 | Syntax for the class of topological bases. |
class TopBases | ||
Definition | df-bases 13683* | Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 13685). Note that "bases" is the plural of "basis". (Contributed by NM, 17-Jul-2006.) |
⊢ TopBases = {𝑥 ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))} | ||
Theorem | isbasisg 13684* | Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.) |
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)))) | ||
Theorem | isbasis2g 13685* | Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.) |
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ (𝑥 ∩ 𝑦)∃𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑥 ∩ 𝑦)))) | ||
Theorem | isbasis3g 13686* | Express the predicate "the set 𝐵 is a basis for a topology". Definition of basis in [Munkres] p. 78. (Contributed by NM, 17-Jul-2006.) |
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ (∀𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝐵∃𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ (𝑥 ∩ 𝑦)∃𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑥 ∩ 𝑦))))) | ||
Theorem | basis1 13687 | Property of a basis. (Contributed by NM, 16-Jul-2006.) |
⊢ ((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → (𝐶 ∩ 𝐷) ⊆ ∪ (𝐵 ∩ 𝒫 (𝐶 ∩ 𝐷))) | ||
Theorem | basis2 13688* | Property of a basis. (Contributed by NM, 17-Jul-2006.) |
⊢ (((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵) ∧ (𝐷 ∈ 𝐵 ∧ 𝐴 ∈ (𝐶 ∩ 𝐷))) → ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷))) | ||
Theorem | fiinbas 13689* | If a set is closed under finite intersection, then it is a basis for a topology. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐵 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ∈ 𝐵) → 𝐵 ∈ TopBases) | ||
Theorem | baspartn 13690* | A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ ((𝑃 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) → 𝑃 ∈ TopBases) | ||
Theorem | tgval2 13691* | Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 13704) that (topGen‘𝐵) is indeed a topology (on ∪ 𝐵, see unitg 13702). See also tgval 12717 and tgval3 13698. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ (𝑥 ⊆ ∪ 𝐵 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐵 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))}) | ||
Theorem | eltg 13692 | Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ 𝐴 ⊆ ∪ (𝐵 ∩ 𝒫 𝐴))) | ||
Theorem | eltg2 13693* | Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ (𝐴 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴)))) | ||
Theorem | eltg2b 13694* | Membership in a topology generated by a basis. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 10-Jan-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴))) | ||
Theorem | eltg4i 13695 | An open set in a topology generated by a basis is the union of all basic open sets contained in it. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (𝐴 ∈ (topGen‘𝐵) → 𝐴 = ∪ (𝐵 ∩ 𝒫 𝐴)) | ||
Theorem | eltg3i 13696 | The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → ∪ 𝐴 ∈ (topGen‘𝐵)) | ||
Theorem | eltg3 13697* | Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Jim Kingdon, 4-Mar-2023.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∃𝑥(𝑥 ⊆ 𝐵 ∧ 𝐴 = ∪ 𝑥))) | ||
Theorem | tgval3 13698* | Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80. See also tgval 12717 and tgval2 13691. (Contributed by NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.) |
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)}) | ||
Theorem | tg1 13699 | Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.) |
⊢ (𝐴 ∈ (topGen‘𝐵) → 𝐴 ⊆ ∪ 𝐵) | ||
Theorem | tg2 13700* | Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.) |
⊢ ((𝐴 ∈ (topGen‘𝐵) ∧ 𝐶 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 (𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |