Access the full text.
Sign up today, get an introductory month for just $19.
Y. Shidama (2004)
Intersections of Intervals and Balls inE n T
Artur Korni, Y. Shidama (2005)
Brouwer Fixed Point Theorem for Disks on the Plane
Wojciech Trybulec (1990)
Vectors in Real Linear Space
Artur Korniłowicz (2004)
Intersections of intervals and balls in ε^{n}/_{T}Formalized Mathematics, 12
Ramez Mousa (2003)
Ordinal Numbers
Yatsuka Nakamura (1999)
Bounded domains and unbounded domainsFormalized Mathematics, 8
Agata Darmochwał (1990)
Compact spacesFormalized Mathematics, 1
Beata Padlewska, Agata Darmochwa (1990)
Topological Spaces and Continuous Functions
Noboru Endou (2003)
Convex sets and convex combinationsFormalized Mathematics, 11
Krzysztof Hryniewiecki (2004)
Basic Properties of Real Numbers
A. Trybulec (1990)
Domains and Their Cartesian Products
A. Trybulec (1991)
A Borsuk Theorem on Homotopy Types
Stanisława Kanas (1990)
Metric spacesFormalized Mathematics, 1
(1979)
Geometria i topologia
AB Collins, D. Alcock (2012)
PrincipalInjury Prevention, 18
M. Wysocki (2004)
Subsets of Topological Spaces1
(1994)
Understanding in mathematics
Noboru Endou (2003)
Dimension of real unitary spaceFormalized Mathematics, 11
(1990)
Agata Darmochwał. Compact spaces. Formalized Mathematics
H. Matsuzaki, N. Endou, Y. Shidama (2008)
Convex Sets and Convex Combinations on Complex Linear Spaces, 16
Agata Darmochwał (1989)
Families of Subsets , Subspaces and Mappings in Topological Spaces
Agata Darmochwał (1991)
The Euclidean spaceFormalized Mathematics, 2
Agata Darmochwa (2018)
The Euclidean SpaceGeometric Concepts for Geometric Design
Edmund Woronowicz (1990)
Relations Defined on Sets
Kenneth August (2011)
CARDINAL NUMBERS
G. Bancerek (1990)
The Fundamental Properties of Natural Numbers
FORMALIZED Vol. MATHEMATICS 19, No. 3, Pages 151153, 2011 DOI: 10.2478/v10037-011-0024-3 Karol Pk Institute of Informatics University of Bialystok Poland Summary. In this article we prove the Brouwer fixed point theorem for an arbitrary convex compact subset of E n with a non empty interior. This article is based on [15]. MML identifier: BROUWER2, version: 7.11.07 4.160.1126 The notation and terminology used here have been introduced in the following papers: [17], [12], [1], [4], [7], [16], [6], [13], [10], [2], [3], [14], [9], [20], [18], [8], [19], [11], [21], and [5]. 1. Preliminaries For simplicity, we adopt the following convention: n is a natural number, p, n n n q, u, w are points of ET , S is a subset of ET , A, B are convex subsets of ET , and r is a real number. Next we state several propositions: (1) (1 - r) · p + r · q = p + r · (q - p). (2) If u, w halfline(p, q) and |u - p| = |w - p|, then u = w. (3) Let given S. Suppose p S and p = q and S halfline(p, q) is Bounded. Then there exists w such that (i) w Fr S halfline(p, q), (ii) for every u such that u S halfline(p, q) holds |p - u| |p - w|, and (iii) for every r such that r > 0 there exists u such that u S halfline(p, q) and |w - u| < r. 151 2011 University of Bialystok ISSN 14262630(p), 1898-9934(e) karol pk (4) For every A such that A is closed and p Int A and p = q and A halfline(p, q) is Bounded there exists u such that Fr Ahalfline(p, q) = {u}. (5) If r > 0, then Fr Ball(p, r) = Sphere(p, r). n Let n be an element of N, let A be a Bounded subset of ET , and let p be a n . One can verify that p + A is Bounded. point of ET 2. Main Theorems Next we state four propositions: n (6) Let n be an element of N and A be a convex subset of ET . Suppose A is compact and non boundary. Then there exists a function h from n n ET A into Tdisk(0ET , 1) such that h is homeomorphism and h Fr A = n ), 1). Sphere((0ET (7) Let given A, B. Suppose A is compact and non boundary and B is n compact and non boundary. Then there exists a function h from ET A n into ET B such that h is homeomorphism and h Fr A = Fr B. (8)1 For every A such that A is compact and non boundary holds every n n continuous function from ET A into ET A has a fixpoint. n (9) Let A be a non empty convex subset of ET . Suppose A is compact and n non boundary. Let F1 be a non empty subspace of ET A. If (F1 ) = Fr A, n A. then F1 is not a retract of ET
Formalized Mathematics – de Gruyter
Published: Jan 1, 2011
You can share this free article with as many people as you like with the url below! We hope you enjoy this feature!
Read and print from thousands of top scholarly journals.
Already have an account? Log in
Bookmark this article. You can see your Bookmarks on your DeepDyve Library.
To save an article, log in first, or sign up for a DeepDyve account if you don’t already have one.
Copy and paste the desired citation format or use the link below to download a file formatted for EndNote
Access the full text.
Sign up today, get an introductory month for just $19.
All DeepDyve websites use cookies to improve your online experience. They were placed on your computer when you launched this website. You can change your cookie settings through your browser.