pith. machine review for the scientific record. sign in
def definition def or abbrev

powerClass

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  87def powerClass : Power → PowerClass
  88  | .telepathy             => .DirectMechanism
  89  | .precognition          => .DirectMechanism
  90  | .empathy               => .DirectMechanism
  91  | .healing               => .DirectMechanism
  92  | .immortality           => .DirectMechanism
  93  | .astralProjection      => .DirectMechanism
  94  | .superIntelligence     => .Derivable
  95  | .enhancedSenses        => .Derivable
  96  | .soundControl          => .Derivable
  97  | .animalCommunication   => .Derivable
  98  | .mindInfluence         => .Derivable
  99  | .collectivePower       => .Derivable
 100  | .flight                => .NautilusClass
 101  | .invulnerability       => .NautilusClass
 102  | .superStrength         => .NautilusClass
 103  | .forceFields           => .NautilusClass
 104  | .energyProjection      => .NautilusClass
 105  | .transmutation         => .NautilusClass
 106  | .timePerception        => .Speculative
 107  | .superSpeed            => .Speculative
 108  | .invisibility          => .Speculative
 109  | .elementalControl      => .Speculative
 110  | .sizeManipulation      => .Speculative
 111  | .duplication           => .Constrained
 112  | .realityWarping        => .Constrained
 113  | .creationExNihilo      => .Constrained
 114  | .absoluteInvulnerability => .Constrained
 115
 116/-- A power is accessible if its class is not Constrained. -/
 117def Power.accessible (p : Power) : Bool := (powerClass p).accessible

proof body

Definition body.

 118
 119/-- List of all 27 powers. -/

used by (8)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.