Blueprint Summary
Overview
Total entries106completed: 106; deps incomplete: 0; sorries: 0; no proof: 0
Ready now0Entries with an actionable next formalization step.
Fully closed106Local code and prerequisite closure are both complete.
Actionable priorities0Entries ready now and already unlocking downstream work.
Entry index (106)
Definitions88completed: 88; deps incomplete: 0; sorries: 0; no proof: 0
Theorems18completed: 18; deps incomplete: 0; sorries: 0; no proof: 0
Definition Index (88)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (11)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (4)
-
Associated lean decls (3)
-
Associated lean decls (5)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (7)
-
Associated lean decls (1)
-
Associated lean decls (6)
-
Associated lean decls (5)
-
Associated lean decls (2)
-
Associated lean decls (5)
-
Associated lean decls (1)
-
Associated lean decls (5)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (18)
-
QuotientSpace.support -
QuotientSpace.fiber -
QuotientSpace.preimage -
QuotientSpace.stalkIdeal -
QuotientSpace.prelocalPred -
QuotientSpace.localPred -
QuotientSpace.sheafTypes -
QuotientSpace.instCommRingObjOppositeOpensCarrierSupportPresheafSheafTypes -
QuotientSpace.sectionsSubring -
QuotientSpace.presheafCommRing -
QuotientSpace.classFamily -
QuotientSpace.classHom -
QuotientSpace.ιTop -
QuotientSpace.ιHom -
QuotientSpace.quotientSpace -
QuotientSpace.ι -
KLocallyRingedSpace.quotient -
KLocallyRingedSpace.quotientι
-
-
Associated lean decls (1)
-
Associated lean decls (6)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (5)
-
Associated lean decls (13)
-
Associated lean decls (8)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (11)
-
KLocallyRingedSpace -
KLocallyRingedSpace.toLocallyRingedSpace -
KLocallyRingedSpace.algebraMap -
KLocallyRingedSpace.Hom -
KLocallyRingedSpace.Hom.toFun -
KLocallyRingedSpace.instCategory -
KLocallyRingedSpace.KIso -
KLocallyRingedSpace.restrictOpen -
KLocallyRingedSpace.ofRestrict -
KLocallyRingedSpace.Hom.ofFac -
KLocallyRingedSpace.instCoeSortType
-
-
Associated lean decls (3)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (5)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (11)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (4)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (12)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (5)
-
Associated lean decls (9)
-
Associated lean decls (3)
-
Associated lean decls (2)
Theorem / Proposition / Lemma / Corollary Index (18)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
Dependency insights
Statement-used entries57Entries reused in statement dependencies.
Proof-used entries70Entries reused in proof-only dependencies.
Most used in statements (57)
-
Reverse dependencies recorded in statement dependencies.statement uses: 25proof uses: 6direct uses: 31downstream unlocks: 43
Associated lean decls (11)
-
Reverse dependencies recorded in statement dependencies.statement uses: 16proof uses: 4direct uses: 20downstream unlocks: 33
-
Reverse dependencies recorded in statement dependencies.statement uses: 16proof uses: 5direct uses: 21downstream unlocks: 23
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 14proof uses: 5direct uses: 19downstream unlocks: 22
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 13proof uses: 8direct uses: 21downstream unlocks: 26
-
Reverse dependencies recorded in statement dependencies.statement uses: 11proof uses: 15direct uses: 26downstream unlocks: 47
Associated lean decls (13)
-
Reverse dependencies recorded in statement dependencies.statement uses: 11proof uses: 4direct uses: 15downstream unlocks: 25
Associated lean decls (12)
-
Reverse dependencies recorded in statement dependencies.statement uses: 10proof uses: 18direct uses: 28downstream unlocks: 45
-
Reverse dependencies recorded in statement dependencies.statement uses: 10proof uses: 1direct uses: 11downstream unlocks: 15
Associated lean decls (5)
-
Reverse dependencies recorded in statement dependencies.statement uses: 8proof uses: 3direct uses: 11downstream unlocks: 13
Associated lean decls (11)
-
KLocallyRingedSpace -
KLocallyRingedSpace.toLocallyRingedSpace -
KLocallyRingedSpace.algebraMap -
KLocallyRingedSpace.Hom -
KLocallyRingedSpace.Hom.toFun -
KLocallyRingedSpace.instCategory -
KLocallyRingedSpace.KIso -
KLocallyRingedSpace.restrictOpen -
KLocallyRingedSpace.ofRestrict -
KLocallyRingedSpace.Hom.ofFac -
KLocallyRingedSpace.instCoeSortType
-
-
Show all 47 more statement-used entries
-
Reverse dependencies recorded in statement dependencies.statement uses: 8proof uses: 1direct uses: 9downstream unlocks: 9
-
Reverse dependencies recorded in statement dependencies.statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 7
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 1direct uses: 7downstream unlocks: 30
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 3direct uses: 9downstream unlocks: 15
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 5direct uses: 9downstream unlocks: 12
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 8
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 4direct uses: 7downstream unlocks: 65
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 6direct uses: 9downstream unlocks: 19
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 3direct uses: 6downstream unlocks: 7
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 1direct uses: 4downstream unlocks: 6
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 1direct uses: 4downstream unlocks: 5
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 5
Associated lean decls (7)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
Associated lean decls (5)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 3direct uses: 5downstream unlocks: 50
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 27
Associated lean decls (5)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 4direct uses: 6downstream unlocks: 10
Associated lean decls (11)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 5direct uses: 7downstream unlocks: 9
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 9
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 3direct uses: 5downstream unlocks: 8
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 3
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 3direct uses: 4downstream unlocks: 36
Associated lean decls (6)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 11direct uses: 12downstream unlocks: 34
Associated lean decls (5)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 4direct uses: 5downstream unlocks: 30
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 4direct uses: 5downstream unlocks: 16
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 11
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 2direct uses: 3downstream unlocks: 4
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 3
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 2
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Most used in proofs (70)
-
Reverse dependencies recorded in proof dependencies.proof uses: 18statement uses: 10direct uses: 28downstream unlocks: 45
-
Reverse dependencies recorded in proof dependencies.proof uses: 15statement uses: 11direct uses: 26downstream unlocks: 47
Associated lean decls (13)
-
Reverse dependencies recorded in proof dependencies.proof uses: 11statement uses: 1direct uses: 12downstream unlocks: 34
Associated lean decls (5)
-
Reverse dependencies recorded in proof dependencies.proof uses: 8statement uses: 13direct uses: 21downstream unlocks: 26
-
Reverse dependencies recorded in proof dependencies.proof uses: 7statement uses: 0direct uses: 7downstream unlocks: 11
Associated lean decls (3)
-
Reverse dependencies recorded in proof dependencies.proof uses: 6statement uses: 25direct uses: 31downstream unlocks: 43
Associated lean decls (11)
-
Reverse dependencies recorded in proof dependencies.proof uses: 6statement uses: 3direct uses: 9downstream unlocks: 19
Associated lean decls (3)
-
Reverse dependencies recorded in proof dependencies.proof uses: 6statement uses: 0direct uses: 6downstream unlocks: 10
Associated lean decls (3)
-
Reverse dependencies recorded in proof dependencies.proof uses: 5statement uses: 16direct uses: 21downstream unlocks: 23
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 5statement uses: 14direct uses: 19downstream unlocks: 22
Associated lean decls (2)
-
Show all 60 more proof-used entries
-
Reverse dependencies recorded in proof dependencies.proof uses: 5statement uses: 4direct uses: 9downstream unlocks: 12
-
Reverse dependencies recorded in proof dependencies.proof uses: 5statement uses: 2direct uses: 7downstream unlocks: 9
-
Reverse dependencies recorded in proof dependencies.proof uses: 4statement uses: 3direct uses: 7downstream unlocks: 65
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 4statement uses: 16direct uses: 20downstream unlocks: 33
-
Reverse dependencies recorded in proof dependencies.proof uses: 4statement uses: 1direct uses: 5downstream unlocks: 30
Associated lean decls (4)
-
Reverse dependencies recorded in proof dependencies.proof uses: 4statement uses: 0direct uses: 4downstream unlocks: 28
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 4statement uses: 11direct uses: 15downstream unlocks: 25
Associated lean decls (12)
-
Reverse dependencies recorded in proof dependencies.proof uses: 4statement uses: 0direct uses: 4downstream unlocks: 18
Associated lean decls (3)
-
Reverse dependencies recorded in proof dependencies.proof uses: 4statement uses: 0direct uses: 4downstream unlocks: 17
Associated lean decls (9)
-
Reverse dependencies recorded in proof dependencies.proof uses: 4statement uses: 1direct uses: 5downstream unlocks: 16
Associated lean decls (4)
-
Reverse dependencies recorded in proof dependencies.proof uses: 4statement uses: 2direct uses: 6downstream unlocks: 10
Associated lean decls (11)
-
Reverse dependencies recorded in proof dependencies.proof uses: 4statement uses: 0direct uses: 4downstream unlocks: 5
Associated lean decls (5)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 2direct uses: 5downstream unlocks: 50
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 1direct uses: 4downstream unlocks: 36
Associated lean decls (6)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 6direct uses: 9downstream unlocks: 15
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 8direct uses: 11downstream unlocks: 13
Associated lean decls (11)
-
KLocallyRingedSpace -
KLocallyRingedSpace.toLocallyRingedSpace -
KLocallyRingedSpace.algebraMap -
KLocallyRingedSpace.Hom -
KLocallyRingedSpace.Hom.toFun -
KLocallyRingedSpace.instCategory -
KLocallyRingedSpace.KIso -
KLocallyRingedSpace.restrictOpen -
KLocallyRingedSpace.ofRestrict -
KLocallyRingedSpace.Hom.ofFac -
KLocallyRingedSpace.instCoeSortType
-
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 2direct uses: 5downstream unlocks: 8
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 3direct uses: 6downstream unlocks: 7
Associated lean decls (3)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 7
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 5
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 4
Associated lean decls (5)
-
Reverse dependencies recorded in proof dependencies.proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 4
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 8
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 6
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 5
Associated lean decls (3)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 1direct uses: 3downstream unlocks: 4
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 4
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 4
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 33
Associated lean decls (4)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 32
Associated lean decls (4)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 31
Associated lean decls (5)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 6direct uses: 7downstream unlocks: 30
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 27
Associated lean decls (5)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 10direct uses: 11downstream unlocks: 15
Associated lean decls (5)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 11
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 10
Associated lean decls (8)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 8direct uses: 9downstream unlocks: 9
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 7
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 3direct uses: 4downstream unlocks: 6
Associated lean decls (3)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 6
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 6
Associated lean decls (6)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 3direct uses: 4downstream unlocks: 5
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 5
Associated lean decls (4)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 5
Associated lean decls (18)
-
QuotientSpace.support -
QuotientSpace.fiber -
QuotientSpace.preimage -
QuotientSpace.stalkIdeal -
QuotientSpace.prelocalPred -
QuotientSpace.localPred -
QuotientSpace.sheafTypes -
QuotientSpace.instCommRingObjOppositeOpensCarrierSupportPresheafSheafTypes -
QuotientSpace.sectionsSubring -
QuotientSpace.presheafCommRing -
QuotientSpace.classFamily -
QuotientSpace.classHom -
QuotientSpace.ιTop -
QuotientSpace.ιHom -
QuotientSpace.quotientSpace -
QuotientSpace.ι -
KLocallyRingedSpace.quotient -
KLocallyRingedSpace.quotientι
-
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 5
Associated lean decls (3)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 3
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 3
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 2
Associated lean decls (2)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in proof dependencies.proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Metadata
Metadata audit
Missing owner106
Missing effort106
Untagged106
Missing owner (106)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (11)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Show all 96 more entries missing owner
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (5)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (5)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (12)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (5)
-
Missing owner metadata.
Associated lean decls (6)
-
Missing owner metadata.
Associated lean decls (5)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (11)
-
KLocallyRingedSpace -
KLocallyRingedSpace.toLocallyRingedSpace -
KLocallyRingedSpace.algebraMap -
KLocallyRingedSpace.Hom -
KLocallyRingedSpace.Hom.toFun -
KLocallyRingedSpace.instCategory -
KLocallyRingedSpace.KIso -
KLocallyRingedSpace.restrictOpen -
KLocallyRingedSpace.ofRestrict -
KLocallyRingedSpace.Hom.ofFac -
KLocallyRingedSpace.instCoeSortType
-
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (8)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (5)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (5)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (18)
-
QuotientSpace.support -
QuotientSpace.fiber -
QuotientSpace.preimage -
QuotientSpace.stalkIdeal -
QuotientSpace.prelocalPred -
QuotientSpace.localPred -
QuotientSpace.sheafTypes -
QuotientSpace.instCommRingObjOppositeOpensCarrierSupportPresheafSheafTypes -
QuotientSpace.sectionsSubring -
QuotientSpace.presheafCommRing -
QuotientSpace.classFamily -
QuotientSpace.classHom -
QuotientSpace.ιTop -
QuotientSpace.ιHom -
QuotientSpace.quotientSpace -
QuotientSpace.ι -
KLocallyRingedSpace.quotient -
KLocallyRingedSpace.quotientι
-
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (9)
-
Missing owner metadata.
Associated lean decls (5)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (11)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (13)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (6)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (7)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing effort (106)
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (11)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Show all 96 more entries missing effort
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (5)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (5)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (12)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (5)
-
Missing effort metadata.
Associated lean decls (6)
-
Missing effort metadata.
Associated lean decls (5)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (11)
-
KLocallyRingedSpace -
KLocallyRingedSpace.toLocallyRingedSpace -
KLocallyRingedSpace.algebraMap -
KLocallyRingedSpace.Hom -
KLocallyRingedSpace.Hom.toFun -
KLocallyRingedSpace.instCategory -
KLocallyRingedSpace.KIso -
KLocallyRingedSpace.restrictOpen -
KLocallyRingedSpace.ofRestrict -
KLocallyRingedSpace.Hom.ofFac -
KLocallyRingedSpace.instCoeSortType
-
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (8)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (5)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (5)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (18)
-
QuotientSpace.support -
QuotientSpace.fiber -
QuotientSpace.preimage -
QuotientSpace.stalkIdeal -
QuotientSpace.prelocalPred -
QuotientSpace.localPred -
QuotientSpace.sheafTypes -
QuotientSpace.instCommRingObjOppositeOpensCarrierSupportPresheafSheafTypes -
QuotientSpace.sectionsSubring -
QuotientSpace.presheafCommRing -
QuotientSpace.classFamily -
QuotientSpace.classHom -
QuotientSpace.ιTop -
QuotientSpace.ιHom -
QuotientSpace.quotientSpace -
QuotientSpace.ι -
KLocallyRingedSpace.quotient -
KLocallyRingedSpace.quotientι
-
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (9)
-
Missing effort metadata.
Associated lean decls (5)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (11)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (13)
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (6)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (7)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Untagged (106)
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (11)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Show all 96 more untagged entries
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (5)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (5)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (12)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (5)
-
Missing tag metadata.
Associated lean decls (6)
-
Missing tag metadata.
Associated lean decls (5)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (11)
-
KLocallyRingedSpace -
KLocallyRingedSpace.toLocallyRingedSpace -
KLocallyRingedSpace.algebraMap -
KLocallyRingedSpace.Hom -
KLocallyRingedSpace.Hom.toFun -
KLocallyRingedSpace.instCategory -
KLocallyRingedSpace.KIso -
KLocallyRingedSpace.restrictOpen -
KLocallyRingedSpace.ofRestrict -
KLocallyRingedSpace.Hom.ofFac -
KLocallyRingedSpace.instCoeSortType
-
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (8)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (5)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (5)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (18)
-
QuotientSpace.support -
QuotientSpace.fiber -
QuotientSpace.preimage -
QuotientSpace.stalkIdeal -
QuotientSpace.prelocalPred -
QuotientSpace.localPred -
QuotientSpace.sheafTypes -
QuotientSpace.instCommRingObjOppositeOpensCarrierSupportPresheafSheafTypes -
QuotientSpace.sectionsSubring -
QuotientSpace.presheafCommRing -
QuotientSpace.classFamily -
QuotientSpace.classHom -
QuotientSpace.ιTop -
QuotientSpace.ιHom -
QuotientSpace.quotientSpace -
QuotientSpace.ι -
KLocallyRingedSpace.quotient -
KLocallyRingedSpace.quotientι
-
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (9)
-
Missing tag metadata.
Associated lean decls (5)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (11)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (13)
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (6)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (7)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Structure and coverage
Fully closed106Local code and ancestor closure are both complete.
Heaviest prerequisites (92)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 14statement deps: 1proof deps: 13direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 12statement deps: 3proof deps: 9direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 12statement deps: 3proof deps: 9direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 12statement deps: 5proof deps: 7direct uses: 2downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 12statement deps: 6proof deps: 6direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 11statement deps: 4proof deps: 7direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 11statement deps: 11proof deps: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 10statement deps: 3proof deps: 7direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 10statement deps: 6proof deps: 4direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 10statement deps: 7proof deps: 3direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Show all 82 more heaviest-prerequisite entries
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 10statement deps: 8proof deps: 2direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 9statement deps: 3proof deps: 6direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 9statement deps: 3proof deps: 6direct uses: 2downstream unlocks: 4
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 9statement deps: 4proof deps: 5direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 9statement deps: 8proof deps: 1direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 9statement deps: 9proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 4proof deps: 4direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 5proof deps: 3direct uses: 2downstream unlocks: 3
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 6proof deps: 2direct uses: 1downstream unlocks: 3
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 8statement deps: 7proof deps: 1direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 2proof deps: 5direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 2proof deps: 5direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 2proof deps: 5direct uses: 3downstream unlocks: 5
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 3proof deps: 4direct uses: 5downstream unlocks: 8
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 3proof deps: 4direct uses: 2downstream unlocks: 4
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 7statement deps: 4proof deps: 3direct uses: 6downstream unlocks: 10
Associated lean decls (11)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 2proof deps: 4direct uses: 2downstream unlocks: 4
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 2proof deps: 4direct uses: 2downstream unlocks: 5
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 3proof deps: 3direct uses: 4downstream unlocks: 17
Associated lean decls (9)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 4proof deps: 2direct uses: 3downstream unlocks: 5
Associated lean decls (7)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 1proof deps: 4direct uses: 4downstream unlocks: 8
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 1proof deps: 4direct uses: 2downstream unlocks: 2
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 2proof deps: 3direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 2proof deps: 3direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 2proof deps: 3direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 2proof deps: 3direct uses: 3downstream unlocks: 27
Associated lean decls (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 3proof deps: 2direct uses: 5downstream unlocks: 16
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 3proof deps: 2direct uses: 2downstream unlocks: 2
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 3proof deps: 2direct uses: 3downstream unlocks: 4
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 4proof deps: 1direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 4proof deps: 1direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 1proof deps: 3direct uses: 3downstream unlocks: 3
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 1proof deps: 3direct uses: 6downstream unlocks: 10
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 1proof deps: 3direct uses: 0downstream unlocks: 0
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 2proof deps: 2direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 2proof deps: 2direct uses: 9downstream unlocks: 15
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 2proof deps: 2direct uses: 3downstream unlocks: 3
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 2proof deps: 2direct uses: 2downstream unlocks: 2
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 3proof deps: 1direct uses: 3downstream unlocks: 4
Associated lean decls (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 3proof deps: 1direct uses: 20downstream unlocks: 33
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 4statement deps: 4proof deps: 0direct uses: 3downstream unlocks: 4
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 1proof deps: 2direct uses: 4downstream unlocks: 6
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 1proof deps: 2direct uses: 3downstream unlocks: 3
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 1proof deps: 2direct uses: 7downstream unlocks: 7
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 1proof deps: 2direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 1proof deps: 2direct uses: 1downstream unlocks: 5
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 2proof deps: 1direct uses: 11downstream unlocks: 15
Associated lean decls (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 2proof deps: 1direct uses: 1downstream unlocks: 10
Associated lean decls (8)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 2proof deps: 1direct uses: 2downstream unlocks: 8
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 3
Associated lean decls (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 15downstream unlocks: 25
Associated lean decls (12)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 11
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 12downstream unlocks: 34
Associated lean decls (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 7downstream unlocks: 9
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 4downstream unlocks: 5
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 0proof deps: 2direct uses: 3downstream unlocks: 7
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 9downstream unlocks: 9
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 2downstream unlocks: 6
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 1proof deps: 1direct uses: 4downstream unlocks: 18
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 7
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 5
Associated lean decls (18)
-
QuotientSpace.support -
QuotientSpace.fiber -
QuotientSpace.preimage -
QuotientSpace.stalkIdeal -
QuotientSpace.prelocalPred -
QuotientSpace.localPred -
QuotientSpace.sheafTypes -
QuotientSpace.instCommRingObjOppositeOpensCarrierSupportPresheafSheafTypes -
QuotientSpace.sectionsSubring -
QuotientSpace.presheafCommRing -
QuotientSpace.classFamily -
QuotientSpace.classHom -
QuotientSpace.ιTop -
QuotientSpace.ιHom -
QuotientSpace.quotientSpace -
QuotientSpace.ι -
KLocallyRingedSpace.quotient -
KLocallyRingedSpace.quotientι
-
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 5
Associated lean decls (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 30
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 32
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 5
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 7downstream unlocks: 30
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 21downstream unlocks: 26
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 31
Associated lean decls (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 28downstream unlocks: 45
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 5downstream unlocks: 50
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 4
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 3
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 0proof deps: 1direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 19downstream unlocks: 22
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 36
Associated lean decls (6)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 3
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 7downstream unlocks: 11
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 6downstream unlocks: 7
Associated lean decls (3)
-
No prerequisites (14)
-
Associated lean decls (11)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (6)
-
Associated lean decls (13)
-
Associated lean decls (11)
-
KLocallyRingedSpace -
KLocallyRingedSpace.toLocallyRingedSpace -
KLocallyRingedSpace.algebraMap -
KLocallyRingedSpace.Hom -
KLocallyRingedSpace.Hom.toFun -
KLocallyRingedSpace.instCategory -
KLocallyRingedSpace.KIso -
KLocallyRingedSpace.restrictOpen -
KLocallyRingedSpace.ofRestrict -
KLocallyRingedSpace.Hom.ofFac -
KLocallyRingedSpace.instCoeSortType
-
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Show all 4 more entries without prerequisites
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
No dependents (14)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Show all 4 more entries without dependents
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-