Persistence Specification

Stable citation identifiers for the Persistence theory.

Each identifier names a public declaration that exists in this repository. The identifiers are generated from the RR.DEFINES annotations in the Lean source and listed here for downstream citation.

def SE.Persistence.Spec.PS_TYPE_CLASSIFICATION : String

Stable citation identifier for Classification.

Equations

• SE.Persistence.Spec.PS_TYPE_CLASSIFICATION = "PS.TYPE.CLASSIFICATION"

def SE.Persistence.Spec.PS_TYPE_CLASSIFICATION_VALUE : String

Stable citation identifier for ClassificationValue.

Equations

• SE.Persistence.Spec.PS_TYPE_CLASSIFICATION_VALUE = "PS.TYPE.CLASSIFICATION_VALUE"

def SE.Persistence.Spec.PS_TYPE_DYNAMICS : String

Stable citation identifier for Dynamics.

Equations

• SE.Persistence.Spec.PS_TYPE_DYNAMICS = "PS.TYPE.DYNAMICS"

def SE.Persistence.Spec.PS_TYPE_REACH : String

Stable citation identifier for Reach.

Equations

• SE.Persistence.Spec.PS_TYPE_REACH = "PS.TYPE.REACH"

def SE.Persistence.Spec.PS_TYPE_GENERATED : String

Stable citation identifier for Generated.

Equations

• SE.Persistence.Spec.PS_TYPE_GENERATED = "PS.TYPE.GENERATED"

def SE.Persistence.Spec.PS_DEF_APPLICABLE : String

Stable citation identifier for Classification.Applicable.

Equations

• SE.Persistence.Spec.PS_DEF_APPLICABLE = "PS.DEF.APPLICABLE"

def SE.Persistence.Spec.PS_DEF_IS_PRS : String

Stable citation identifier for Classification.IsPrs.

Equations

• SE.Persistence.Spec.PS_DEF_IS_PRS = "PS.DEF.IS_PRS"

def SE.Persistence.Spec.PS_DEF_IS_BRK : String

Stable citation identifier for Classification.IsBrk.

Equations

• SE.Persistence.Spec.PS_DEF_IS_BRK = "PS.DEF.IS_BRK"

def SE.Persistence.Spec.PS_DEF_WELL_FORMED : String

Stable citation identifier for Classification.WellFormed.

Equations

• SE.Persistence.Spec.PS_DEF_WELL_FORMED = "PS.DEF.WELL_FORMED"

def SE.Persistence.Spec.PS_DEF_COARSE : String

Stable citation identifier for Classification.coarse.

Equations

• SE.Persistence.Spec.PS_DEF_COARSE = "PS.DEF.COARSE"

def SE.Persistence.Spec.PS_DEF_LIFT_FAMILY : String

Stable citation identifier for Classification.liftFamily.

Equations

• SE.Persistence.Spec.PS_DEF_LIFT_FAMILY = "PS.DEF.LIFT_FAMILY"

def SE.Persistence.Spec.PS_DEF_LIFT_KIND : String

Stable citation identifier for Classification.liftKind.

Equations

• SE.Persistence.Spec.PS_DEF_LIFT_KIND = "PS.DEF.LIFT_KIND"

def SE.Persistence.Spec.PS_DEF_REFERENCE_CLASSIFICATION_VALUES : String

Stable citation identifier for referenceClassificationValues.

Equations

• SE.Persistence.Spec.PS_DEF_REFERENCE_CLASSIFICATION_VALUES = "PS.DEF.REFERENCE_CLASSIFICATION_VALUES"

def SE.Persistence.Spec.PS_DEF_STEP_BRK : String

Stable citation identifier for Classification.stepBrk.

Equations

• SE.Persistence.Spec.PS_DEF_STEP_BRK = "PS.DEF.STEP_BRK"

def SE.Persistence.Spec.PS_DEF_IDENTITY_REL : String

Stable citation identifier for Classification.identityRel.

Equations

• SE.Persistence.Spec.PS_DEF_IDENTITY_REL = "PS.DEF.IDENTITY_REL"

def SE.Persistence.Spec.PS_DEF_FREE_DYNAMICS : String

Stable citation identifier for freeDynamics.

Equations

• SE.Persistence.Spec.PS_DEF_FREE_DYNAMICS = "PS.DEF.FREE_DYNAMICS"

def SE.Persistence.Spec.PS_DEF_INVARIANT : String

Stable citation identifier for Classification.Invariant.

Equations

• SE.Persistence.Spec.PS_DEF_INVARIANT = "PS.DEF.INVARIANT"

def SE.Persistence.Spec.PS_DEF_NON_COLLAPSING : String

Stable citation identifier for Classification.NonCollapsing.

Equations

• SE.Persistence.Spec.PS_DEF_NON_COLLAPSING = "PS.DEF.NON_COLLAPSING"

def SE.Persistence.Spec.PS_DEF_STEP_REL : String

Stable citation identifier for Classification.stepRel.

Equations

• SE.Persistence.Spec.PS_DEF_STEP_REL = "PS.DEF.STEP_REL"

def SE.Persistence.Spec.PS_DEF_SURVIVES : String

Stable citation identifier for Classification.Survives.

Equations

• SE.Persistence.Spec.PS_DEF_SURVIVES = "PS.DEF.SURVIVES"

def SE.Persistence.Spec.PS_THM_APPLICABLE_IFF : String

Stable citation identifier for Classification.applicable_iff.

Equations

• SE.Persistence.Spec.PS_THM_APPLICABLE_IFF = "PS.THM.APPLICABLE_IFF"

def SE.Persistence.Spec.PS_THM_NOT_IS_PRS_OF_IS_BRK : String

Stable citation identifier for Classification.not_isPrs_of_isBrk.

Equations

• SE.Persistence.Spec.PS_THM_NOT_IS_PRS_OF_IS_BRK = "PS.THM.NOT_IS_PRS_OF_IS_BRK"

def SE.Persistence.Spec.PS_THM_COARSE_EQ_PRS_IFF : String

Stable citation identifier for Classification.coarse_eq_prs_iff.

Equations

• SE.Persistence.Spec.PS_THM_COARSE_EQ_PRS_IFF = "PS.THM.COARSE_EQ_PRS_IFF"

def SE.Persistence.Spec.PS_THM_LIFT_FAMILY_PATTERN_EQ : String

Stable citation identifier for Classification.liftFamily_pattern_eq.

Equations

• SE.Persistence.Spec.PS_THM_LIFT_FAMILY_PATTERN_EQ = "PS.THM.LIFT_FAMILY_PATTERN_EQ"

def SE.Persistence.Spec.PS_THM_LIFT_KIND_PATTERN_EQ : String

Stable citation identifier for Classification.liftKind_pattern_eq.

Equations

• SE.Persistence.Spec.PS_THM_LIFT_KIND_PATTERN_EQ = "PS.THM.LIFT_KIND_PATTERN_EQ"

def SE.Persistence.Spec.PS_THM_NOT_IDENTITY_REL_OF_STEP_BRK_FREE : String

Stable citation identifier for Classification.not_identityRel_of_stepBrk_free.

Equations

• SE.Persistence.Spec.PS_THM_NOT_IDENTITY_REL_OF_STEP_BRK_FREE = "PS.THM.NOT_IDENTITY_REL_OF_STEP_BRK_FREE"

def SE.Persistence.Spec.PS_THM_IDENTITY_REL_EQUIVALENCE : String

Stable citation identifier for Classification.identityRel_equivalence.

Equations

• SE.Persistence.Spec.PS_THM_IDENTITY_REL_EQUIVALENCE = "PS.THM.IDENTITY_REL_EQUIVALENCE"

def SE.Persistence.Spec.PS_THM_SURVIVES_IDENTITY_REL : String

Stable citation identifier for Classification.survives_identityRel.

Equations

• SE.Persistence.Spec.PS_THM_SURVIVES_IDENTITY_REL = "PS.THM.SURVIVES_IDENTITY_REL"

def SE.Persistence.Spec.PS_THM_IDENTITY_REL_MONO : String

Stable citation identifier for Classification.identityRel_mono.

Equations

• SE.Persistence.Spec.PS_THM_IDENTITY_REL_MONO = "PS.THM.IDENTITY_REL_MONO"

def SE.Persistence.Spec.PS_THM_IDENTITY_REL_EQ_OF_PRS_IFF : String

Stable citation identifier for Classification.identityRel_eq_of_prs_iff.

Equations

• SE.Persistence.Spec.PS_THM_IDENTITY_REL_EQ_OF_PRS_IFF = "PS.THM.IDENTITY_REL_EQ_OF_PRS_IFF"

def SE.Persistence.Spec.PS_THM_IDENTITY_REL_EQ_OF_COARSE_EQ : String

Stable citation identifier for Classification.identityRel_eq_of_coarse_eq.

Equations

• SE.Persistence.Spec.PS_THM_IDENTITY_REL_EQ_OF_COARSE_EQ = "PS.THM.IDENTITY_REL_EQ_OF_COARSE_EQ"

def SE.Persistence.Spec.PS_THM_IDENTITY_REL_FREE_IFF : String

Stable citation identifier for Classification.identityRel_free_iff.

Equations

• SE.Persistence.Spec.PS_THM_IDENTITY_REL_FREE_IFF = "PS.THM.IDENTITY_REL_FREE_IFF"

def SE.Persistence.Spec.PS_THM_INVARIANT_IFF_RESPECTS_IDENTITY_REL : String

Stable citation identifier for Classification.invariant_iff_respects_identityRel.

Equations

• SE.Persistence.Spec.PS_THM_INVARIANT_IFF_RESPECTS_IDENTITY_REL = "PS.THM.INVARIANT_IFF_RESPECTS_IDENTITY_REL"

def SE.Persistence.Spec.PS_THM_INVARIANT_OF_PRS_SUBSET : String

Stable citation identifier for Classification.invariant_of_prs_subset.

Equations

• SE.Persistence.Spec.PS_THM_INVARIANT_OF_PRS_SUBSET = "PS.THM.INVARIANT_OF_PRS_SUBSET"

def SE.Persistence.Spec.PS_THM_PRS_DIFFERENCE_OF_NON_COLLAPSING : String

Stable citation identifier for Classification.prs_difference_of_nonCollapsing.

Equations

• SE.Persistence.Spec.PS_THM_PRS_DIFFERENCE_OF_NON_COLLAPSING = "PS.THM.PRS_DIFFERENCE_OF_NON_COLLAPSING"

def SE.Persistence.Spec.PS_THM_NON_COLLAPSING_FREE_IFF : String

Stable citation identifier for Classification.nonCollapsing_free_iff.

Equations

• SE.Persistence.Spec.PS_THM_NON_COLLAPSING_FREE_IFF = "PS.THM.NON_COLLAPSING_FREE_IFF"

def SE.Persistence.Spec.PS_THM_SURVIVES_NE_IDENTITY_REL_FREE : String

Stable citation identifier for Classification.survives_ne_identityRel_free.

Equations

• SE.Persistence.Spec.PS_THM_SURVIVES_NE_IDENTITY_REL_FREE = "PS.THM.SURVIVES_NE_IDENTITY_REL_FREE"

def SE.Persistence.Spec.PS_THM_STEP_BRK_NOT_SEPARATING : String

Stable citation identifier for Classification.stepBrk_not_separating.

Equations

• SE.Persistence.Spec.PS_THM_STEP_BRK_NOT_SEPARATING = "PS.THM.STEP_BRK_NOT_SEPARATING"

def SE.Persistence.Spec.PS_THM_SURVIVES_MONO : String

Stable citation identifier for Classification.survives_mono.

Equations

• SE.Persistence.Spec.PS_THM_SURVIVES_MONO = "PS.THM.SURVIVES_MONO"