Documentation

LeanPool.NFWeakPartition.NFStandard.HailperinUnitUnion

NF weak partition development: NFStandard.HailperinUnitUnion.

typeLower turns a relation-like object R into the set of z for which every pair ⟨w,{z}⟩ belongs to R. Taking R = V × (V \ A) and then a complement therefore removes exactly one singleton level from the membership test.

source
noncomputable def NFChoice.Foundation.NFStandard.unitUnionObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (A : S.carrier) :
S.carrier

Remove one singleton level from the elements tested against A.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem NFChoice.Foundation.NFStandard.mem_unitUnionObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (A z : S.carrier) :
    SemanticCore.Mem S z (unitUnionObj hH A) ↔ SemanticCore.Mem S (singleton hH z) A

    Exact semantic law for one level of singleton lowering.

    source
    noncomputable def NFChoice.Foundation.NFStandard.unitUnionIter {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) :
    ℕ → S.carrier → S.carrier

    Iterate singleton lowering m times.

    Equations
    Instances For
      source
      @[simp]
      theorem NFChoice.Foundation.NFStandard.unitUnionIter_zero {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (A : S.carrier) :
      unitUnionIter hH 0 A = A
      source
      @[simp]
      theorem NFChoice.Foundation.NFStandard.unitUnionIter_succ {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m : ℕ) (A : S.carrier) :
      unitUnionIter hH (m + 1) A = unitUnionIter hH m (unitUnionObj hH A)
      source
      @[simp]
      theorem NFChoice.Foundation.NFStandard.mem_unitUnionIter {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m : ℕ) (A z : S.carrier) :
      SemanticCore.Mem S z (unitUnionIter hH m A) ↔ SemanticCore.Mem S (raise hH m z) A

      Iterated lowering is inverse, at the membership level, to raise.