Induction

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

Statistics

Metric	Count
Definitions ι	1
Theorems freeOfProfinite, isClosedEmbedding, P0, Plimit, linearIndependent, linearIndependentAux, Nobeling_aux	7
Total	8

LocallyConstant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
freeOfProfinite 📖	mathematical	—	Module.Free LocallyConstant TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str Int.instSemiring instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule instAddCommGroup Int.instAddCommGroup	—	exists_wellOrder Profinite.NobelingProof.Nobeling_aux Profinite.Nobeling.isClosedEmbedding

Profinite.Nobeling

Definitions

Name	Category	Theorems
ι 📖	CompOp	1 math math: isClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosedEmbedding 📖	mathematical	—	Topology.IsClosedEmbedding TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str Pi.topologicalSpace Set IsClopen instTopologicalSpaceBool ι	—	Continuous.isClosedEmbedding CompHausLike.is_compact Pi.t2Space TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.DiscreteTopology.metrizableSpace instDiscreteTopologyBool continuous_pi IsLocallyConstant.iff_continuous List.TFAE.out IsLocallyConstant.tfae IsClopen.isOpen isClopen_compl_iff Set.ext exists_isClopen_of_totally_separated instTotallySeparatedSpaceOfTotallyDisconnectedSpace WeaklyLocallyCompactSpace.locallyCompactSpace T2Space.r1Space CompHausLike.is_hausdorff instWeaklyLocallyCompactSpaceOfCompactSpace Profinite.instTotallyDisconnectedSpaceCarrierToTop

Profinite.NobelingProof

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Nobeling_aux 📖	mathematical	Topology.IsClosedEmbedding TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str Pi.topologicalSpace instTopologicalSpaceBool	Module.Free LocallyConstant Int.instSemiring LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup	—	Module.Free.of_equiv' Module.Free.of_basis Topology.IsClosedEmbedding.isClosed_range RingHomInvPair.ids Topology.IsClosedEmbedding.isEmbedding

Profinite.NobelingProof.GoodProducts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
P0 📖	mathematical	—	Profinite.NobelingProof.P Ordinal Ordinal.zero	—	isWellOrder_lt not_lt_zero Ordinal.canonicallyOrderedAdd Set.subset_singleton_iff_eq linearIndependentEmpty linearIndependentSingleton
Plimit 📖	—	Order.IsSuccLimit Ordinal PartialOrder.toPreorder Ordinal.partialOrder Profinite.NobelingProof.P	—	—	isWellOrder_lt linearIndependent_iff_union_smaller linearIndependent_subtype_iff linearIndepOn_iUnion_of_directed Monotone.directed_le SemilatticeSup.instIsDirectedOrder smaller_mono linearIndependent_iff_smaller LE.le.trans LT.lt.le Profinite.NobelingProof.isClosed_proj Profinite.NobelingProof.contained_proj
linearIndependent 📖	mathematical	—	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	—	linearIndependentAux isWellOrder_lt le_refl Ordinal.typein_lt_type
linearIndependentAux 📖	mathematical	—	Profinite.NobelingProof.P	—	P0 isWellOrder_lt lt_of_lt_of_le Order.lt_succ Ordinal.instNoMaxOrder linearIndependent_iff_sum ModuleCat.linearIndependent_leftExact Profinite.NobelingProof.succ_exact le_of_lt Profinite.NobelingProof.isClosed_proj Profinite.NobelingProof.contained_proj linearIndependent_comp_of_eval span Profinite.NobelingProof.isClosed_C' Profinite.NobelingProof.contained_C' Profinite.NobelingProof.succ_mono square_commutes Plimit

---

← Back to Index