Successor

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

Statistics

Metric	Count
Definitions C', C0, C1, CC'₀, CC'₁, MaxProducts, MaxToGood, SumEval, sum_equiv, sum_to, Linear_CC', Linear_CC'₀, Linear_CC'₁, Tail, SwapTrue	15
Theorems C0_projOrd, C1_projOrd, CC_comp_zero, CC_exact, chain'_cons_of_lt, good_lt_maxProducts, head!_eq_o_of_maxProducts, injective_sum_to, isChain_cons_of_lt, linearIndependent_comp_of_eval, linearIndependent_iff_sum, maxTail_isGood, maxToGood_injective, max_eq_eval, max_eq_eval_unapply, max_eq_o_cons_tail, span_sum, square_commutes, sum_equiv_comp_eval_eq_elim, sum_to_range, union_succ, evalCons, max_eq_eval, max_eq_o_cons_tail, max_eq_o_cons_tail', contained_C', contained_C1, continuous_CC'₀, continuous_CC'₁, continuous_swapTrue, isClosed_C', isClosed_C0, isClosed_C1, mem_C'_eq_false, succ_exact, succ_mono, swapTrue_eq_true, swapTrue_mem_C1, union_C0C1_eq	39
Total	54

Profinite.NobelingProof

Definitions

Name	Category	Theorems
C' 📖	CompOp	11 math math: Products.max_eq_eval, succ_exact, continuous_CC'₁, GoodProducts.maxToGood_injective, GoodProducts.maxTail_isGood, isClosed_C', contained_C', CC_comp_zero, continuous_CC'₀, GoodProducts.max_eq_eval, GoodProducts.max_eq_eval_unapply
C0 📖	CompOp	2 math math: isClosed_C0, union_C0C1_eq
C1 📖	CompOp	4 math math: union_C0C1_eq, contained_C1, swapTrue_mem_C1, isClosed_C1
CC'₀ 📖	CompOp	1 math math: continuous_CC'₀
CC'₁ 📖	CompOp	1 math math: continuous_CC'₁
Linear_CC' 📖	CompOp	6 math math: Products.max_eq_eval, GoodProducts.linearIndependent_comp_of_eval, succ_exact, CC_comp_zero, GoodProducts.max_eq_eval, GoodProducts.max_eq_eval_unapply
Linear_CC'₀ 📖	CompOp	—
Linear_CC'₁ 📖	CompOp	—
SwapTrue 📖	CompOp	3 math, 1 bridge math: continuous_swapTrue, C1_projOrd, swapTrue_mem_C1 bridge: swapTrue_eq_true

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C0_projOrd 📖	mathematical	contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt Set Set.instMembership C0	Proj ord LinearOrder.toDecidableLT Ordinal.instLinearOrder	—	isWellOrder_lt LE.le.lt_or_eq Ordinal.instNoMaxOrder not_imp_not ord_term
C1_projOrd 📖	mathematical	contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt Set Set.instMembership C1	SwapTrue Proj ord LinearOrder.toDecidableLT Ordinal.instLinearOrder	—	isWellOrder_lt ord_term lt_of_le_of_ne Ordinal.instNoMaxOrder not_imp_not
CC_comp_zero 📖	mathematical	contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	DFunLike.coe LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring LocallyConstant Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool C' LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup LinearMap.instFunLike Linear_CC' π ord LinearOrder.toDecidableLT Ordinal.instLinearOrder πs LocallyConstant.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing	—	isWellOrder_lt LocallyConstant.ext if_ctx_congr LT.lt.ne
CC_exact 📖	mathematical	contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt DFunLike.coe LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring LocallyConstant Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool C' LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup LinearMap.instFunLike Linear_CC' LocallyConstant.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing	π ord LinearOrder.toDecidableLT Ordinal.instLinearOrder πs	—	isWellOrder_lt Subtype.prop continuous_induced_dom swapTrue_mem_C1 Continuous.comp continuous_swapTrue continuous_subtype_val C0_projOrd union_C0C1_eq isClosed_C0 isClosed_proj isClosed_C1 continuous_CC'₁ continuous_CC'₀ LocallyConstant.ext LocallyConstant.piecewise'_apply_left LocallyConstant.piecewise'_apply_right C1_projOrd
contained_C' 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	contained C'	—	isWellOrder_lt contained_C1
contained_C1 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	contained π C1 ord LinearOrder.toDecidableLT Ordinal.instLinearOrder	—	isWellOrder_lt contained_proj
continuous_CC'₀ 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	Continuous Set.Elem C' instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool CC'₀	—	isWellOrder_lt continuous_subtype_val
continuous_CC'₁ 📖	mathematical	contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	Continuous Set.Elem C' instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool CC'₁	—	isWellOrder_lt Continuous.comp continuous_swapTrue continuous_subtype_val
continuous_swapTrue 📖	mathematical	—	Continuous Pi.topologicalSpace instTopologicalSpaceBool SwapTrue	—	continuous_pi Continuous.comp' continuous_bot continuous_apply
isClosed_C' 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	IsClosed Pi.topologicalSpace instTopologicalSpaceBool C'	—	isWellOrder_lt IsClosed.inter isClosed_C0 isClosed_proj isClosed_C1
isClosed_C0 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	IsClosed Pi.topologicalSpace instTopologicalSpaceBool C0	—	isWellOrder_lt IsClosed.inter continuous_apply IsClosed.preimage isClosed_discrete instDiscreteTopologyBool
isClosed_C1 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	IsClosed Pi.topologicalSpace instTopologicalSpaceBool C1	—	isWellOrder_lt IsClosed.inter continuous_apply IsClosed.preimage isClosed_discrete instDiscreteTopologyBool
mem_C'_eq_false 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt Set Set.instMembership C'	term	—	isWellOrder_lt ord_term_aux
succ_exact 📖	mathematical	contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	CategoryTheory.ShortComplex.Exact ModuleCat Int.instRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ModuleCat.of LocallyConstant Set.Elem π ord LinearOrder.toDecidableLT Ordinal.instLinearOrder instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool LocallyConstant.instAddCommGroup Int.instAddCommGroup AddCommGroup.toIntModule C' ModuleCat.ofHom πs Linear_CC'	—	isWellOrder_lt CategoryTheory.ShortComplex.moduleCat_exact_iff CC_exact
succ_mono 📖	mathematical	—	CategoryTheory.Mono ModuleCat Int.instRing ModuleCat.moduleCategory ModuleCat.of LocallyConstant Set.Elem π Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder ord LinearOrder.toDecidableLT Ordinal.instLinearOrder instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool LocallyConstant.instAddCommGroup Int.instAddCommGroup AddCommGroup.toIntModule ModuleCat.ofHom πs	—	ModuleCat.mono_iff_injective injective_πs
swapTrue_eq_true 📖	bridging (complete)	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	SwapTrue term	SwapTrue	isWellOrder_lt ord_term_aux
swapTrue_mem_C1 📖	mathematical	contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	Set Set.instMembership C1 SwapTrue π ord LinearOrder.toDecidableLT Ordinal.instLinearOrder	—	isWellOrder_lt ord_term Mathlib.Tactic.Contrapose.contrapose₃ Order.succ_le_of_lt LE.le.lt_of_ne'
union_C0C1_eq 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	Set Set.instUnion C0 C1	—	isWellOrder_lt Set.ext Bool.dichotomy

Profinite.NobelingProof.GoodProducts

Definitions

Name	Category	Theorems
MaxProducts 📖	CompOp	15 math math: sum_to_range, linearIndependent_comp_of_eval, span_sum, injective_sum_to, good_lt_maxProducts, union_succ, linearIndependent_iff_sum, square_commutes, maxToGood_injective, maxTail_isGood, max_eq_o_cons_tail, sum_equiv_comp_eval_eq_elim, max_eq_eval, head!_eq_o_of_maxProducts, max_eq_eval_unapply
MaxToGood 📖	CompOp	1 math math: maxToGood_injective
SumEval 📖	CompOp	3 math math: linearIndependent_comp_of_eval, linearIndependent_iff_sum, square_commutes
sum_equiv 📖	CompOp	1 math math: sum_equiv_comp_eval_eq_elim
sum_to 📖	CompOp	2 math math: sum_to_range, injective_sum_to

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
chain'_cons_of_lt 📖	mathematical	Profinite.NobelingProof.contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt Profinite.NobelingProof.Products Profinite.NobelingProof.Products.instLinearOrder Profinite.NobelingProof.Products.Tail Set Set.instMembership MaxProducts	Profinite.NobelingProof.term	—	isChain_cons_of_lt
good_lt_maxProducts 📖	mathematical	Profinite.NobelingProof.contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	Profinite.NobelingProof.Products Set Set.instMembership Profinite.NobelingProof.GoodProducts Profinite.NobelingProof.π Profinite.NobelingProof.ord LinearOrder.toDecidableLT Ordinal.instLinearOrder MaxProducts	—	isWellOrder_lt max_eq_o_cons_tail List.cons_head!_tail Ordinal.typein_lt_typein Ordinal.typein_enum Profinite.NobelingProof.Products.prop_of_isGood Subtype.prop List.head!_mem_self
head!_eq_o_of_maxProducts 📖	mathematical	Profinite.NobelingProof.contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	Profinite.NobelingProof.Products Set Set.instMembership MaxProducts Profinite.NobelingProof.term	—	isWellOrder_lt Profinite.NobelingProof.ord_term Subtype.prop Profinite.NobelingProof.Products.prop_of_isGood_of_contained List.head!_mem_self eq_of_le_of_not_lt Ordinal.instNoMaxOrder not_lt Profinite.NobelingProof.Products.rel_head!_of_mem Profinite.NobelingProof.ord_term_aux
injective_sum_to 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	Set.Elem Profinite.NobelingProof.Products Profinite.NobelingProof.GoodProducts Profinite.NobelingProof.π Profinite.NobelingProof.ord LinearOrder.toDecidableLT Ordinal.instLinearOrder MaxProducts sum_to	—	isWellOrder_lt Function.Injective.sumElim Subtype.val_injective Profinite.NobelingProof.Products.prop_of_isGood Profinite.NobelingProof.ord_term_aux
isChain_cons_of_lt 📖	mathematical	Profinite.NobelingProof.contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt Profinite.NobelingProof.Products Profinite.NobelingProof.Products.instLinearOrder Profinite.NobelingProof.Products.Tail Set Set.instMembership MaxProducts	Profinite.NobelingProof.term	—	isWellOrder_lt lt_of_le_of_lt Profinite.NobelingProof.Products.rel_head!_of_mem Profinite.NobelingProof.Products.head!_le_of_lt Profinite.NobelingProof.Products.lt_iff_lex_lt Subtype.prop max_eq_o_cons_tail List.head!_mem_self
linearIndependent_comp_of_eval 📖	mathematical	Profinite.NobelingProof.contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt Submodule LocallyConstant Set.Elem Profinite.NobelingProof.π Profinite.NobelingProof.ord LinearOrder.toDecidableLT Ordinal.instLinearOrder instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool Int.instSemiring LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup Preorder.toLE Submodule.instPartialOrder Top.top Submodule.instTop Submodule.span Set.range Profinite.NobelingProof.Products Profinite.NobelingProof.Products.isGood eval LinearIndependent Profinite.NobelingProof.C'	MaxProducts ModuleCat.carrier Int.instRing ModuleCat.of DFunLike.coe CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.ofHom Profinite.NobelingProof.Linear_CC' Profinite.NobelingProof.GoodProducts SumEval	—	isWellOrder_lt max_eq_eval_unapply maxToGood_injective LinearIndependent.comp
linearIndependent_iff_sum 📖	mathematical	Profinite.NobelingProof.contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	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 Profinite.NobelingProof.GoodProducts Profinite.NobelingProof.π Profinite.NobelingProof.ord LinearOrder.toDecidableLT Ordinal.instLinearOrder MaxProducts SumEval	—	isWellOrder_lt linearIndependent_equiv SumEval.eq_1 sum_equiv_comp_eval_eq_elim
maxTail_isGood 📖	mathematical	Profinite.NobelingProof.contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt Submodule LocallyConstant Set.Elem Profinite.NobelingProof.π Profinite.NobelingProof.ord LinearOrder.toDecidableLT Ordinal.instLinearOrder instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool Int.instSemiring LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup Preorder.toLE Submodule.instPartialOrder Top.top Submodule.instTop Submodule.span Set.range Profinite.NobelingProof.Products Profinite.NobelingProof.Products.isGood eval	Profinite.NobelingProof.C' Profinite.NobelingProof.Products.Tail MaxProducts	—	isWellOrder_lt max_eq_eval Finsupp.mem_span_image_iff_linearCombination Finsupp.linearCombination_apply map_finsuppSum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.sum_congr map_smul SemilinearMapClass.toMulActionSemiHomClass Finsupp.mem_supported isChain_cons_of_lt Subtype.coe_eta Profinite.NobelingProof.Products.max_eq_eval Profinite.NobelingProof.Products.max_eq_o_cons_tail Profinite.NobelingProof.succ_exact RingHomSurjective.ids CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker LinearMap.sub_mem_ker_iff Submodule.mem_top Finsupp.mem_span_range_iff_exists_finsupp Subtype.prop eq_sub_iff_add_eq Submodule.add_mem Submodule.finsuppSum_mem Submodule.smul_mem Submodule.subset_span Profinite.NobelingProof.Products.eval_πs Profinite.NobelingProof.Products.prop_of_isGood good_lt_maxProducts Finsupp.mem_support_iff max_eq_o_cons_tail Profinite.NobelingProof.Products.lt_iff_lex_lt
maxToGood_injective 📖	mathematical	Profinite.NobelingProof.contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt Submodule LocallyConstant Set.Elem Profinite.NobelingProof.π Profinite.NobelingProof.ord LinearOrder.toDecidableLT Ordinal.instLinearOrder instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool Int.instSemiring LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup Preorder.toLE Submodule.instPartialOrder Top.top Submodule.instTop Submodule.span Set.range Profinite.NobelingProof.Products Profinite.NobelingProof.Products.isGood eval	MaxProducts Profinite.NobelingProof.GoodProducts Profinite.NobelingProof.C' MaxToGood	—	isWellOrder_lt max_eq_o_cons_tail
max_eq_eval 📖	mathematical	Profinite.NobelingProof.contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	DFunLike.coe LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring LocallyConstant Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool Profinite.NobelingProof.C' LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup LinearMap.instFunLike Profinite.NobelingProof.Linear_CC' Profinite.NobelingProof.Products.eval Profinite.NobelingProof.Products MaxProducts Profinite.NobelingProof.Products.Tail	—	isWellOrder_lt Profinite.NobelingProof.Products.max_eq_eval Subtype.prop head!_eq_o_of_maxProducts
max_eq_eval_unapply 📖	mathematical	Profinite.NobelingProof.contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	Set.Elem Profinite.NobelingProof.Products MaxProducts LocallyConstant instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool Profinite.NobelingProof.C' DFunLike.coe LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup LinearMap.instFunLike Profinite.NobelingProof.Linear_CC' Profinite.NobelingProof.Products.eval Profinite.NobelingProof.Products.Tail	—	isWellOrder_lt max_eq_eval
max_eq_o_cons_tail 📖	mathematical	Profinite.NobelingProof.contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	Profinite.NobelingProof.Products Set Set.instMembership MaxProducts Profinite.NobelingProof.term Profinite.NobelingProof.Products.Tail	—	isWellOrder_lt Profinite.NobelingProof.Products.max_eq_o_cons_tail Subtype.prop head!_eq_o_of_maxProducts
span_sum 📖	mathematical	Profinite.NobelingProof.contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	Set.range LocallyConstant Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool Profinite.NobelingProof.Products Profinite.NobelingProof.Products.isGood eval Profinite.NobelingProof.GoodProducts Profinite.NobelingProof.π Profinite.NobelingProof.ord LinearOrder.toDecidableLT Ordinal.instLinearOrder MaxProducts Profinite.NobelingProof.Products.eval	—	isWellOrder_lt sum_equiv_comp_eval_eq_elim Equiv.toFun_as_coe EquivLike.range_comp
square_commutes 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	Set.Elem Profinite.NobelingProof.Products Profinite.NobelingProof.GoodProducts Profinite.NobelingProof.π Profinite.NobelingProof.ord LinearOrder.toDecidableLT Ordinal.instLinearOrder MaxProducts LocallyConstant instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool SumEval Profinite.NobelingProof.Products.isGood ModuleCat.carrier Int.instRing ModuleCat.of LocallyConstant.instAddCommGroup Int.instAddCommGroup AddCommGroup.toIntModule DFunLike.coe CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.ofHom Profinite.NobelingProof.πs eval	—	isWellOrder_lt LocallyConstant.ext Profinite.NobelingProof.Products.eval_πs Profinite.NobelingProof.Products.prop_of_isGood Subtype.prop
sum_equiv_comp_eval_eq_elim 📖	mathematical	Profinite.NobelingProof.contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	Set.Elem Profinite.NobelingProof.Products Profinite.NobelingProof.GoodProducts Profinite.NobelingProof.π Profinite.NobelingProof.ord LinearOrder.toDecidableLT Ordinal.instLinearOrder MaxProducts Profinite.NobelingProof.Products.isGood LocallyConstant instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool eval Equiv.toFun sum_equiv Profinite.NobelingProof.Products.eval	—	isWellOrder_lt LocallyConstant.ext
sum_to_range 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	Set.range Profinite.NobelingProof.Products Set.Elem Profinite.NobelingProof.GoodProducts Profinite.NobelingProof.π Profinite.NobelingProof.ord LinearOrder.toDecidableLT Ordinal.instLinearOrder MaxProducts sum_to Set Set.instUnion	—	isWellOrder_lt Set.Sum.elim_range Subtype.range_coe_subtype
union_succ 📖	mathematical	Profinite.NobelingProof.contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	Profinite.NobelingProof.GoodProducts Set Profinite.NobelingProof.Products Set.instUnion Profinite.NobelingProof.π Profinite.NobelingProof.ord LinearOrder.toDecidableLT Ordinal.instLinearOrder MaxProducts	—	isWellOrder_lt Set.ext Profinite.NobelingProof.Products.prop_of_isGood_of_contained LE.le.lt_of_ne Ordinal.instNoMaxOrder Profinite.NobelingProof.ord_term Profinite.NobelingProof.Products.eval_πs_image Profinite.NobelingProof.Products.eval_πs Submodule.apply_mem_span_image_iff_mem_span RingHomSurjective.ids Profinite.NobelingProof.injective_πs Profinite.NobelingProof.Products.isGood_mono LT.lt.le Order.lt_succ Profinite.NobelingProof.contained_eq_proj

Profinite.NobelingProof.Products

Definitions

Name	Category	Theorems
Tail 📖	CompOp	6 math math: max_eq_eval, Profinite.NobelingProof.GoodProducts.maxTail_isGood, Profinite.NobelingProof.GoodProducts.max_eq_o_cons_tail, max_eq_o_cons_tail, Profinite.NobelingProof.GoodProducts.max_eq_eval, Profinite.NobelingProof.GoodProducts.max_eq_eval_unapply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
evalCons 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	eval LocallyConstant Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool LocallyConstant.instMul Profinite.NobelingProof.e List.IsChain.sublist instTransGT	—	—
max_eq_eval 📖	mathematical	Profinite.NobelingProof.contained Order.succ Ordinal PartialOrder.toPreorder Ordinal.partialOrder Ordinal.instSuccOrder Preorder.toLT Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt Profinite.NobelingProof.term	DFunLike.coe LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring LocallyConstant Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool Profinite.NobelingProof.C' LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup LinearMap.instFunLike Profinite.NobelingProof.Linear_CC' eval Tail	—	isWellOrder_lt max_eq_o_cons_tail Subtype.prop max_eq_o_cons_tail' List.IsChain.sublist evalCons LocallyConstant.ext Profinite.NobelingProof.continuous_CC'₁ Profinite.NobelingProof.continuous_CC'₀ Subtype.coe_eta Profinite.NobelingProof.CC'₁.eq_1 Profinite.NobelingProof.CC'₀.eq_1 eval_eq mul_ite mul_one MulZeroClass.mul_zero Profinite.NobelingProof.ord_term LT.lt.ne List.IsChain.rel_cons Profinite.NobelingProof.swapTrue_eq_true Profinite.NobelingProof.mem_C'_eq_false Mathlib.Tactic.Push.not_forall_eq
max_eq_o_cons_tail 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt Profinite.NobelingProof.term	Tail	—	isWellOrder_lt List.cons_head!_tail
max_eq_o_cons_tail' 📖	—	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt Profinite.NobelingProof.term Tail	—	—	isWellOrder_lt max_eq_o_cons_tail Subtype.coe_eta

---

← Back to Index