Documentation Verification Report

ZeroLimit

📁 Source: Mathlib/Topology/Category/Profinite/Nobeling/ZeroLimit.lean

Statistics

Metric	Count
Definitions `range_equiv`, `range_equiv_smaller`, `range_equiv_smaller_toFun`, `smaller`, `nil`, `instUniqueSubtypeProductsIsGoodSingletonForallBoolSetFalse`	6
Theorems `linearIndependentEmpty`, `linearIndependentSingleton`, `linearIndependent_iff_smaller`, `linearIndependent_iff_union_smaller`, `range_equiv_factorization`, `range_equiv_smaller_toFun_bijective`, `smaller_factorization`, `smaller_mono`, `union`, `isGood_nil`, `limitOrdinal`, `lt_nil_empty`, `span_nil_eq_top`, `instIsAddTorsionFreeLocallyConstantInt`, `instIsEmptySubtypeProductsIsGoodEmptyCollectionSetForallBool`, `instNontrivialLocallyConstantIntOfNonempty`, `instSubsingletonLocallyConstantElemForallBoolEmptyCollectionSetInt`	17
Total	23

Profinite.NobelingProof

Definitions

Name	Category	Theorems
`instUniqueSubtypeProductsIsGoodSingletonForallBoolSetFalse` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsAddTorsionFreeLocallyConstantInt` 📖	mathematical	—	`IsAddTorsionFree` `LocallyConstant` `LocallyConstant.instAddMonoid` `Int.instAddMonoid`	—	`Function.Injective.isAddTorsionFree` `Pi.instIsAddTorsionFree` `Int.instIsAddTorsionFree` `LocallyConstant.coe_injective`
`instIsEmptySubtypeProductsIsGoodEmptyCollectionSetForallBool` 📖	mathematical	—	`IsEmpty` `Products` `Products.isGood` `Set` `Set.instEmptyCollection`	—	`isEmpty_iff` `subsingleton_iff` `instSubsingletonLocallyConstantElemForallBoolEmptyCollectionSetInt` `Submodule.zero_mem`
`instNontrivialLocallyConstantIntOfNonempty` 📖	mathematical	—	`Nontrivial` `LocallyConstant`	—	`Function.const_injective` `zero_ne_one`
`instSubsingletonLocallyConstantElemForallBoolEmptyCollectionSetInt` 📖	mathematical	—	`LocallyConstant` `Set.Elem` `Set` `Set.instEmptyCollection` `instTopologicalSpaceSubtype` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool`	—	`subsingleton_iff` `LocallyConstant.ext` `Set.instIsEmptyElemEmptyCollection`

Profinite.NobelingProof.GoodProducts

Definitions

Name	Category	Theorems
`range_equiv` 📖	CompOp	1 math math: `range_equiv_factorization`
`range_equiv_smaller` 📖	CompOp	1 math math: `smaller_factorization`
`range_equiv_smaller_toFun` 📖	CompOp	1 math math: `range_equiv_smaller_toFun_bijective`
`smaller` 📖	CompOp	7 math math: `linearIndependent_iff_union_smaller`, `range_equiv_factorization`, `smaller_factorization`, `linearIndependent_iff_smaller`, `smaller_mono`, `range_equiv_smaller_toFun_bijective`, `union`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearIndependentEmpty` 📖	mathematical	—	`LinearIndependent` `Profinite.NobelingProof.Products` `Profinite.NobelingProof.Products.isGood` `Set` `Set.instEmptyCollection` `LocallyConstant` `Set.Elem` `instTopologicalSpaceSubtype` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `eval` `Int.instSemiring` `LocallyConstant.instAddCommMonoid` `Int.instAddCommMonoid` `AddCommGroup.toIntModule` `LocallyConstant.instAddCommGroup` `Int.instAddCommGroup`	—	`linearIndependent_empty_type` `Profinite.NobelingProof.instIsEmptySubtypeProductsIsGoodEmptyCollectionSetForallBool`
`linearIndependentSingleton` 📖	mathematical	—	`LinearIndependent` `Profinite.NobelingProof.Products` `Profinite.NobelingProof.Products.isGood` `Set` `Set.instSingletonSet` `LocallyConstant` `Set.Elem` `instTopologicalSpaceSubtype` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `eval` `Int.instSemiring` `LocallyConstant.instAddCommMonoid` `Int.instAddCommMonoid` `AddCommGroup.toIntModule` `LocallyConstant.instAddCommGroup` `Int.instAddCommGroup`	—	`LinearIndependent.of_subsingleton` `Int.instIsDomain` `instIsTorsionFreeIntOfIsAddTorsionFree` `Profinite.NobelingProof.instIsAddTorsionFreeLocallyConstantInt` `Unique.instSubsingleton` `NeZero.one` `Profinite.NobelingProof.instNontrivialLocallyConstantIntOfNonempty`
`linearIndependent_iff_smaller` 📖	mathematical	—	`LinearIndependent` `Profinite.NobelingProof.Products` `Profinite.NobelingProof.Products.isGood` `Profinite.NobelingProof.π` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Profinite.NobelingProof.ord` `LinearOrder.toDecidableLT` `Ordinal.instLinearOrder` `LocallyConstant` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `eval` `Int.instSemiring` `LocallyConstant.instAddCommMonoid` `Int.instAddCommMonoid` `AddCommGroup.toIntModule` `LocallyConstant.instAddCommGroup` `Int.instAddCommGroup` `smaller`	—	`linearIndependent_iff_range` `LinearMap.linearIndependent_iff` `LinearMap.ker_eq_bot_of_injective` `Profinite.NobelingProof.injective_πs` `smaller_factorization` `linearIndependent_equiv`
`linearIndependent_iff_union_smaller` 📖	mathematical	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Profinite.NobelingProof.contained`	`LinearIndependent` `Profinite.NobelingProof.Products` `Profinite.NobelingProof.Products.isGood` `LocallyConstant` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `eval` `Int.instSemiring` `LocallyConstant.instAddCommMonoid` `Int.instAddCommMonoid` `AddCommGroup.toIntModule` `LocallyConstant.instAddCommGroup` `Int.instAddCommGroup` `Set.iUnion` `Preorder.toLT` `smaller`	—	`linearIndependent_iff_range` `range_equiv_factorization` `linearIndependent_equiv`
`range_equiv_factorization` 📖	mathematical	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Profinite.NobelingProof.contained`	`Set.Elem` `LocallyConstant` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `range` `Set.iUnion` `Preorder.toLT` `smaller` `Equiv.toFun` `range_equiv`	—	—
`range_equiv_smaller_toFun_bijective` 📖	mathematical	—	`Function.Bijective` `Set.Elem` `LocallyConstant` `Profinite.NobelingProof.π` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Profinite.NobelingProof.ord` `LinearOrder.toDecidableLT` `Ordinal.instLinearOrder` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `range` `smaller` `range_equiv_smaller_toFun`	—	`Profinite.NobelingProof.injective_πs`
`smaller_factorization` 📖	mathematical	—	`Set.Elem` `LocallyConstant` `Profinite.NobelingProof.π` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Profinite.NobelingProof.ord` `LinearOrder.toDecidableLT` `Ordinal.instLinearOrder` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `range` `smaller` `Equiv.toFun` `range_equiv_smaller` `DFunLike.coe` `LinearMap` `Int.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LocallyConstant.instAddCommMonoid` `Int.instAddCommMonoid` `AddCommGroup.toIntModule` `LocallyConstant.instAddCommGroup` `Int.instAddCommGroup` `LinearMap.instFunLike` `Profinite.NobelingProof.πs`	—	—
`smaller_mono` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`Set` `LocallyConstant` `Set.Elem` `instTopologicalSpaceSubtype` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `Set.instHasSubset` `smaller`	—	`Profinite.NobelingProof.Products.isGood_mono` `LocallyConstant.ext` `eval.eq_1` `Profinite.NobelingProof.Products.eval_πs'` `Profinite.NobelingProof.Products.prop_of_isGood` `Profinite.NobelingProof.coe_πs` `LocallyConstant.toFun_eq_coe` `lt_of_lt_of_le` `Profinite.NobelingProof.coe_πs'` `Function.comp_assoc` `Profinite.NobelingProof.projRestricts_comp_projRestrict`
`union` 📖	mathematical	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Profinite.NobelingProof.contained`	`range` `Set.iUnion` `LocallyConstant` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `Preorder.toLT` `smaller`	—	`Set.ext` `Profinite.NobelingProof.Products.limitOrdinal` `Profinite.NobelingProof.contained_eq_proj` `Profinite.NobelingProof.Products.eval_πs` `Profinite.NobelingProof.Products.prop_of_isGood` `Profinite.NobelingProof.Products.isGood_mono` `le_of_lt`

Profinite.NobelingProof.Products

Definitions

Name	Category	Theorems
`nil` 📖	CompOp	3 math math: `span_nil_eq_top`, `isGood_nil`, `lt_nil_empty`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isGood_nil` 📖	mathematical	—	`isGood` `Set` `Set.instSingletonSet` `nil`	—	`Set.image_congr` `Set.image_empty` `Submodule.span_empty` `NeZero.one` `Profinite.NobelingProof.instNontrivialLocallyConstantIntOfNonempty`
`limitOrdinal` 📖	mathematical	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`isGood` `Profinite.NobelingProof.π` `Preorder.toLT` `Profinite.NobelingProof.ord` `LinearOrder.toDecidableLT` `Ordinal.instLinearOrder`	—	`Finset.sup_lt_iff` `Order.IsSuccLimit.bot_lt` `Order.IsSuccLimit.succ_lt` `prop_of_isGood` `Ordinal.instNoMaxOrder` `le_rfl` `le_of_lt` `eval_πs_image'` `eval_πs'` `Submodule.apply_mem_span_image_iff_mem_span` `RingHomSurjective.ids` `Profinite.NobelingProof.injective_πs'` `isGood_mono`
`lt_nil_empty` 📖	mathematical	—	`setOf` `Profinite.NobelingProof.Products` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `nil` `Set` `Set.instEmptyCollection`	—	`Set.ext`
`span_nil_eq_top` 📖	mathematical	—	`Submodule.span` `LocallyConstant` `Set.Elem` `Set` `Set.instSingletonSet` `instTopologicalSpaceSubtype` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `Int.instSemiring` `LocallyConstant.instAddCommMonoid` `Int.instAddCommMonoid` `AddCommGroup.toIntModule` `LocallyConstant.instAddCommGroup` `Int.instAddCommGroup` `Set.image` `Profinite.NobelingProof.Products` `eval` `nil` `Top.top` `Submodule` `Submodule.instTop`	—	`Set.image_singleton` `eq_top_iff` `Submodule.mem_span_singleton` `zsmul_eq_mul` `mul_one` `LocallyConstant.ext` `Unique.instSubsingleton`

---

← Back to Index