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

ReligiousExperienceCert

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)

  49structure ReligiousExperienceCert where
  50  five_types : Fintype.card ReligiousExperienceType = 5
  51  four_marks : fourMarks = 5 - 1
  52  noetic_quality : Jcost 1 = 0
  53  transiency : ∀ {ε : ℝ}, 0 < ε → Jcost (1 + ε) > 0
  54

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.