Contribution: ZornsLemma

Zorn's Lemma

Authors

Description

This library develops some basic set theory. The main purpose I had in writing it was as support for the Topology library.

Keywords

set theory, cardinals, ordinals, finite, countable, quotients, well orders, zorn's lemma

README

This library develops some basic set theory.  The main purpose I had
in writing it was as support for the Topology library.

Contents, in alphabetical order except where I group related files together:

Cardinals.v - cardinalities of sets
Ordinals.v - a construction of the ordinals without reference to well-orders

Classical_Wf.v - proofs of the classical equivalence of wellfoundedness,
                 the minimal element property, and the descending sequence
                 property

CSB.v - the Cantor-Schroeder-Bernstein theorem

DecidableDec.v - classic_dec: forall P:Prop, {P} + {~P}.

DependentTypeChoice.v - choice on a relation (forall a:A, B a -> Prop)

EnsemblesImplicit.v - settings for appropriate implicit parameters for the
                      standard library's Ensembles functions
ImageImplicit.v - same for the standard library's Sets/Image
Relation_Definitions_Implicit.v - same for the standard library's
                                  Relation_Definitions

EnsemblesSpec.v - defines a notation for e.g. [ n:nat | n > 5 /\ even n ] :
                  Ensemble nat.

EnsemblesUtf8.v - optional UTF-8 notations for set operations

Families.v - operations on families of subsets of X, i.e. Ensemble (Ensemble X)
IndexedFamilies.v - same for indexed families A -> Ensemble X

FiniteIntersections.v - defines the finite intersections of a family of
                        subsets

FiniteTypes.v - definitions and results about finite types
CountableTypes.v - same for countable types
InfiniteTypes.v - same for infinite types

FunctionProperties.v - injective, surjective, etc.

InverseImage.v - inverse images of subsets under functions

Proj1SigInjective.v - inclusion of { x:X | P x } into X is injective 

Quotients.v - quotients by equivalence relations, and induced functions
              on them

WellOrders.v - some basic properties of well-orders, including a proof that
               Zorn's Lemma implies the well-ordering principle

ZornsLemma.v - proof that choice implies Zorn's Lemma

Author: Daniel Schepler

Copyright:
ZornsLemma Coq contribution
Copyright (C) 2011  Daniel Schepler

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 2.1 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA

Available files