InverseLimit

📁 Source: FLT/Patching/Utils/InverseLimit.lean

Statistics

Metric	Count
Definitions InverseLimit	1
Theorems denseRange_inverseLimit, dense_inverseLimit_of_forall_image_dense, nonempty_inverseLimit_of_finite	3
Total	4

(root)

Definitions

Name	Category	Theorems
InverseLimit 📖	CompOp	27 math math: InverseLimit.div₀_def, InverseLimit.lift_continuous, InverseLimit.smul_def, InverseLimit.npow_def, InverseLimit.instIsTopologicalGroup, InverseLimit.natCast_def, InverseLimit.zsmul_def, InverseLimit.inv_def, InverseLimit.mul_def, InverseLimit.nsmul_def, InverseLimit.inv₀_def, InverseLimit.add_def, InverseLimit.instNontrivial, InverseLimit.instIsTopologicalModule, InverseLimit.zpow₀_def, InverseLimit.InverseLimit_def, InverseLimit.instIsTopologicalRing, InverseLimit.one_def, InverseLimit.vadd_def, InverseLimit.zpow_def, InverseLimit.val_continuous, InverseLimit.zero_def, InverseLimit.sub_def, InverseLimit.toComponent_continuous, InverseLimit.neg_def, InverseLimit.intCast_def, InverseLimit.div_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
denseRange_inverseLimit 📖	—	—	—	—	dense_inverseLimit_of_forall_image_dense
dense_inverseLimit_of_forall_image_dense 📖	—	—	—	—	—
nonempty_inverseLimit_of_finite 📖	—	—	—	—	—

---

← Back to Index