Suchergebnisse

Ergebnisse 1 - 10 von 111 :

  • Cartesian product x
  • Algebra und Zahlentheorie x
Alle zurücksetzen
Cartesian Products of Family of Real Linear Spaces

Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics , 1( 1 ):223-230, 1990. [14] Jan Popiołek. Real normed space. Formalized Mathematics , 2( 1 ):111-115, 1991. [15] Yasunari Shidama. Banach space of bounded linear operators. Formalized Mathematics , 12( 1 ):39-48, 2004. [16] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics , 1( 1 ):115-122, 1990. [17] Wojciech A. Trybulec. Pigeon hole

Open access
Topological Manifolds

] Agata Darmochwał. Finite sets. Formalized Mathematics , 1(1):165–167, 1990. [13] Agata Darmochwał. Families of subsets, subspaces and mappings in topological spaces. Formalized Mathematics , 1(2):257–261, 1990. [14] Ryszard Engelking. Teoria wymiaru . PWN, 1981. [15] Adam Grabowski. Properties of the product of compact topological spaces. Formalized Mathematics , 8(1):55–59, 1999. [16] Zbigniew Karno. Separated and weakly separated subspaces of topological spaces. Formalized Mathematics , 2(5):665–674, 1991. [17] Artur Korniłowicz. Jordan curve theorem

Open access
Products in Categories without Uniqueness of cod and dom

Summary

The paper introduces Cartesian products in categories without uniqueness of cod and dom. It is proven that set-theoretical product is the product in the category Ens [7].

Open access
Probability Measure on Discrete Spaces and Algebra of Real-Valued Random Variables

-65, 1990. [5] Czesław Byliński. Functions from a set to a set. Formalized Mathematics , 1( 1 ):153-164, 1990. [6] Czesław Byliński. Partial functions. Formalized Mathematics , 1( 2 ):357-367, 1990. [7] Czesław Byliński. Some basic properties of sets. Formalized Mathematics , 1( 1 ):47-53, 1990. [8] Czesław Byliński. The sum and product of finite sequences of real numbers. Formalized Mathematics , 1( 4 ):661-668, 1990. [9] Agata Darmochwał

Open access
Double Sequences and Iterated Limits in Regular Space

Abstract

First, we define in Mizar [5], the Cartesian product of two filters bases and the Cartesian product of two filters. After comparing the product of two Fréchet filters on ℕ (F1) with the Fréchet filter on ℕ × ℕ (F2), we compare limF₁ and limF₂ for all double sequences in a non empty topological space.

Endou, Okazaki and Shidama formalized in [14] the “convergence in Pringsheim’s sense” for double sequence of real numbers. We show some basic correspondences between the p-convergence and the filter convergence in a topological space. Then we formalize that the double sequence converges in “Pringsheim’s sense” but not in Frechet filter on ℕ × ℕ sense.

In the next section, we generalize some definitions: “is convergent in the first coordinate”, “is convergent in the second coordinate”, “the lim in the first coordinate of”, “the lim in the second coordinate of” according to [14], in Hausdorff space.

Finally, we generalize two theorems: (3) and (4) from [14] in the case of double sequences and we formalize the “iterated limit” theorem (“Double limit” [7], p. 81, par. 8.5 “Double limite” [6] (TG I,57)), all in regular space. We were inspired by the exercises (2.11.4), (2.17.5) [17] and the corrections B.10 [18].

Open access
Basic Operations on Preordered Coherent Spaces

, 6(1):117-121, 1997. [9] Zbigniew Karno. Separated and weakly separated subspaces of topological spaces. Formalized Mathematics , 2(5):665-674, 1991. [10] Artur Korniłowicz. Cartesian products of relations and relational structures. Formalized Mathematics , 6(1):145-152, 1997. [11] J.L. Krivine. Lambda-calculus, types and models. Ellis & Horwood, 1993. [12] Beata Madras. Product of family of universal algebras. Formalized Mathematics , 4(1):103-108, 1993

Open access
Definition of Flat Poset and Existence Theorems for Recursive Call

chain-complete posets. Formalized Mathematics, 18(1):47-51, 2010. doi:10.2478/v10037-010-0006-x. [16] Artur Korniłowicz. Cartesian products of relations and relational structures. Formalized Mathematics, 6(1):145-152, 1997. [17] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1): 115-122, 1990. [18] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97-105, 1990. [19] Wojciech A. Trybulec and Grzegorz Bancerek. Kuratowski - Zorn

Open access
Arithmetic Operations on Functions from Sets into Functional Sets

properties of rational numbers. Formalized Mathematics , 1(5):841-845, 1990. [6] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics , 1(1):97-105, 1990. [7] Andrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics , 11(4):341-347, 2003. [8] Michał J. Trybulec. Integers. Formalized Mathematics , 1(3):501-505, 1990. [9] Zinaida Trybulec. Properties of subsets. Formalized Mathematics , 1(1):67-71, 1990

Open access
Z-modules

-367, 1990. Czesław Byliński. Some basic properties of sets. Formalized Mathematics , 1( 1 ):47-53, 1990. Daniele Micciancio and Shafi Goldwasser. Complexity of lattice problems: A cryptographic perspective (the international series in engineering and computer science). 2002. Christoph Schwarzweller. The binomial theorem for algebraic structures. Formalized Mathematics , 9( 3 ):559-564, 2001. Andrzej Trybulec. Domains and their Cartesian products. Formalized

Open access
Labelled State Transition Systems

(1):165-167, 1990. [10] Karol Pąk. The Catalan numbers. Part II. Formalized Mathematics , 14(4):153-159, 2006, doi:10.2478/v10037-006-0019-7. [11] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics , 1(1):115-122, 1990. [12] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics , 1(1):97-105, 1990. [13] Michał Trybulec. Formal languages - concatenation and closure. Formalized Mathematics , 15(1):11-15, 2007, doi:10

Open access