Theorem implication relation type

Record a genuine theorem implication that is not part of the target definition; these edges may point toward a weaker structure.

Directed semantics

Every direct mAtlas edge is an authored sourcetarget assertion of this type.

Term code
theorem-implication
Source role
Implies by theorem
Target role
Follows by theorem from
Direct relations in this release
78
Predecessor-level policy
none
Prerequisite traversal
none

Machine-readable record

/data/latest/relation-types/theorem-implication.json provides this definition and the IDs of every direct relation of this type.

A path may traverse an edge backwards for connectivity, but that never reverses the authored source-to-target assertion.