meta.yml

---
fullname: Zorn's Lemma
shortname: zorns-lemma
organization: coq-community
coq-community: true

synopsis: This library develops some basic set theory.

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

authors:
- name: Daniel Schepler
  e-mail: dschepler@gmail.com
  initial: true

maintainers:
- name: Andrew Miloradovsky
  nickname: amiloradovsky

opam-file-maintainer: miloradovsky@gmail.com

license:
  fullname: GNU Lesser General Public License v2.1 or later
  identifier: LGPL-2.1-or-later
  file: COPYING

supported_coq_versions:
  text: Coq 8.6 or later
  opam: '{(>= "8.10 & < "8.12~") | (= "dev")}'

tested_coq_nix_versions:
- version_or_url: https://github.com/coq/coq-on-cachix/tarball/master
- version_or_url: "8.11"
- version_or_url: "8.10"

tested_coq_opam_versions:
- version: dev

namespace: ZornsLemma

keywords:
- name: set theory
- name: cardinals
- name: ordinals
- name: finite
- name: countable
- name: quotients
- name: well-orders
- name: Zorn's lemma

categories:
- name: Mathematics/Logic/Set theory

documentation: |

  ## Contents

  In alphabetical order, except where related files are grouped 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

  ## 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
---