ZFLean

TheoremZFLean#

Develops a practical ZFC set-theory framework with von Neumann naturals, integers, rationals, functions, embeddings, isomorphisms, booleans, and sums.

Quoted from the card LeanPool/projects/zflean.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

• ZFSet.isIso_of_biembedding (theorem; a main declaration), declared in LeanPool/ZFLean/Isomorphisms.lean, line 143: “Proves a Cantor-Bernstein theorem for ZF sets.”
• ZFSet.ZFNat.induction (theorem; a main declaration), declared in LeanPool/ZFLean/Naturals.lean, line 319: “Provides induction for the von Neumann natural numbers.”
• ZFSet.ZFInt.induction (theorem; a main declaration), declared in LeanPool/ZFLean/Integers.lean, line 570: “Provides induction for the quotient construction of ZF integers.”

Project

• Authors: Vincent Trélat.
• Source: Set Theory by Thomas Jech, https://doi.org/10.1007/3-540-44761-X.
• Project repository: VTrelat/ZFLean.
• Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
• License: Apache-2.0.
• MSC2020: 03E30, 03B35.
• In Lean Pool: LeanPool/ZFLean, from the card LeanPool/projects/zflean.yaml.

Sources

• Lean Pool at 2b205bf9: LeanPool/projects/zflean.yaml
• Lean Pool at 2b205bf9: LeanPool/ZFLean

LeanZFSet.isIso_of_biembedding · ZFSet.ZFNat.induction · ZFSet.ZFInt.induction

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.