Documentation

LeanPool.NFWeakPartition.ClassBoundaryCoreDev006

NF weak partition development: ClassBoundaryCoreDev006.

source
@[reducible, inline]
abbrev NFChoice.DirectCertificate.ClassBoundaryCoreDev006.Theory :
Fol.SentTheory Foundation.LNF

Proof-translation construction identified upstream as Theory.

Equations
Instances For
    source
    def NFChoice.DirectCertificate.ClassBoundaryCoreDev006.classEq (P Q : Fol.formula Foundation.LNF) :
    Fol.formula Foundation.LNF

    Proof-translation construction identified upstream as classEq.

    Equations
    Instances For
      source
      def NFChoice.DirectCertificate.ClassBoundaryCoreDev006.classMem (P Q : Fol.formula Foundation.LNF) :
      Fol.formula Foundation.LNF

      Proof-translation construction identified upstream as classMem.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def NFChoice.DirectCertificate.ClassBoundaryCoreDev006.literalAxExtProof :
        Fol.prf Theory.fst (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axExt))

        Proof-translation construction identified upstream as literalAxExtProof.

        Equations
        Instances For
          source
          theorem NFChoice.DirectCertificate.ClassBoundaryCoreDev006.literalAxExtFlypitch :
          Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axExt) = ((Fol.preformula.all (Fol.biimp (ClassBoundaryNormalizationDev005.mem &0 &2) (ClassBoundaryNormalizationDev005.mem &0 &1))).imp (Fol.preformula.equal &1 &0)).all.all
          source
          theorem NFChoice.DirectCertificate.ClassBoundaryCoreDev006.liftTwoSubstOne (s t : Fol.term Foundation.LNF) :
          Fol.substTerm (s ↑ 2) t 1 = s ↑ 1
          source
          noncomputable def NFChoice.DirectCertificate.ClassBoundaryCoreDev006.axExtAt (s t : Fol.term Foundation.LNF) :
          Fol.prf Theory.fst (Fol.preformula.imp (ClassBoundaryNormalizationDev005.represents s (ClassBoundaryNormalizationDev005.cvPred t)) (Fol.preformula.equal s t))

          Proof-translation construction identified upstream as axExtAt.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def NFChoice.DirectCertificate.ClassBoundaryCoreDev006.classMemCv (x : Fol.term Foundation.LNF) (Q : Fol.formula Foundation.LNF) :
            Fol.prf Theory.fst (Fol.biimp (classMem (ClassBoundaryNormalizationDev005.cvPred x) Q) (ClassBoundaryNormalizationDev005.applyPred Q x))

            The one extensionality kernel shared by df-clab, df-cleq, and df-clel.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For