OAI/Analysis/CStarAlgebra/PureInfiniteness/Main.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MainGap.Manuscript.CuntzLE line 15

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:308 (same declaration text).

  2. def OAI.MainGap.Manuscript.ProperlyInfinite line 19

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:312 (same declaration text).

  3. def OAI.MainGap.Manuscript.PropertyP line 23

    Also declared: ComparatorChallenges/IndividualStrongInfiniteness.lean:316 (same declaration text).

  4. lemma OAI.MainGap.Manuscript.finiteCuntzLE_of_stable line 26
  5. lemma OAI.MainGap.Manuscript.PropertyP.finite line 33
  6. theorem OAI.MainGap.Manuscript.individual_to_strong line 37
  7. theorem OAI.MainGap.Manuscript.individual_to_strong_spi line 40
  8. theorem OAI.MainGap.Manuscript.individual_to_strong_main line 43

    Distinct definitions of this name: ComparatorChallenges/IndividualStrongInfiniteness.lean:319 (same statement text; different proof or body). Qualify references as OAI.MainGap.Manuscript.individual_to_strong_main@path.