Standalone Lean project
A completed formalization of the difficult part of the consistency proof for Quine's New Foundations set theory.
Flagship declarations
ConNF.BaseAction.smul_nearLitter_of_smul_litter
Project documentation
The main lemma about how approximations interact with actions.
Source project: Con(NF)
Person-level attribution pending.
ConNF.BasePerm.smul_interference
Plain-language statement
Base permutations commute with the interference of near-litters.
Source project: Con(NF)
Person-level attribution pending.
ConNF.card_tSet_le
Plain-language statement
Note that we cannot prove the reverse implication because all of our hypotheses at this stage are about permutations, not objects.
Source project: Con(NF)
Person-level attribution pending.
ConNF.StrAction.flexApprox_coherent
Plain-language statement
TODO: Put this in the blueprint.
Source project: Con(NF)
Person-level attribution pending.
ConNF.Support.supports_coe
Plain-language statement
The same as ModelData but without the propositions. -/ class PreModelData (α : TypeIndex) where TSet : Type u AllPerm : Type u [allPermGroup : Group AllPerm] [allAction : MulAction AllPerm TSet] tSetForget : TSet → StrSet α allPermForget : AllPerm → StrPerm α export PreModelData (TSet AllPerm) attribute [instance] PreModelData.allPermGroup PreModelData....
Source project: Con(NF)
Person-level attribution pending.
Rel.categorise_permutativeExtension_of_oneOne
Plain-language statement
TODO: Strengthen statement in blueprint version.
Source project: Con(NF)
Person-level attribution pending.
Project index
Showing 1 of 1 additional declarations. Use project search for the complete index.
Rel.codomEqDom_iff'
Plain-language statement
An elementary description of the property CodomEqDom.
Source project: Con(NF)
Person-level attribution pending.