IsDirectLimitRestricted

📁 Source: FLT/DedekindDomain/FiniteAdeleRing/IsDirectLimitRestricted.lean

Statistics

Metric	Count
Definitions	0
Theorems directed, instDirectedSystem, instDirectedSystemCoeSubmoduleCoeLinearMapIdInclusionLinearMap, instDirectedSystemOrderDualElemSetSetsCoeSubmodulePrincipalValMemCoeLinearMapIdInclusionLinearMap, instIsDirectLimit, instIsDirectLimit', instNonemptyOrderDualElemSetSets_fLT	7
Total	7

RestrictedProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
directed 📖	—	—	—	—	—
instDirectedSystem 📖	—	—	—	—	—
instDirectedSystemCoeSubmoduleCoeLinearMapIdInclusionLinearMap 📖	mathematical	—	inclusionLinearMap	—	—
instDirectedSystemOrderDualElemSetSetsCoeSubmodulePrincipalValMemCoeLinearMapIdInclusionLinearMap 📖	mathematical	—	inclusionLinearMap	—	instDirectedSystem
instIsDirectLimit 📖	mathematical	—	IsDirectLimit inclusionLinearMap instDirectedSystemCoeSubmoduleCoeLinearMapIdInclusionLinearMap	—	instDirectedSystemCoeSubmoduleCoeLinearMapIdInclusionLinearMap
instIsDirectLimit' 📖	mathematical	—	IsDirectLimit inclusionLinearMap instDirectedSystemOrderDualElemSetSetsCoeSubmodulePrincipalValMemCoeLinearMapIdInclusionLinearMap	—	instIsDirectLimit instNonemptyOrderDualElemSetSets_fLT directed
instNonemptyOrderDualElemSetSets_fLT 📖	—	—	—	—	—

---

← Back to Index