Basic

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

Statistics

Metric	Count
Definitions GoodProducts, equiv_range, eval, range, P, eval, instLinearOrder, isGood, Proj, ProjRestrict, ProjRestricts, contained, e, iso_map, ord, spanCone, spanCone_isLimit, spanFunctor, spanFunctorIsoIndexFunctor, term, π, πs, πs'	23
Theorems equiv_toFun_eq_eval, injective, linearIndependent_iff_range, span_iff_products, evalFacProp, evalFacProps, eval_eq, eval_πs, eval_πs', eval_πs_image, eval_πs_image', head!_le_of_lt, head_lt_ord_of_isGood, instWellFoundedLT, isGood_mono, lt_iff_lex_lt, lt_ord_of_lt, prop_of_isGood, prop_of_isGood_of_contained, rel_head!_of_mem, ProjRestrict_coe, ProjRestricts_coe, coe_πs, coe_πs', contained_eq_proj, contained_proj, continuous_proj, continuous_projRestrict, continuous_projRestricts, injective_πs, injective_πs', isClosed_proj, iso_map_bijective, ord_term, ord_term_aux, projRestricts_comp_projRestrict, projRestricts_eq_comp, projRestricts_eq_id, proj_comp_of_subset, proj_eq_of_subset, proj_eq_self, proj_prop_eq_self, spanFunctorIsoIndexFunctor_hom_app_hom_hom_apply_coe, spanFunctorIsoIndexFunctor_inv_app, surjective_projRestricts, term_ord_aux, πs'_apply_apply, πs_apply_apply	48
Total	71

Profinite.NobelingProof

Definitions

Name	Category	Theorems
GoodProducts 📖	CompOp	11 math math: GoodProducts.sum_to_range, GoodProducts.linearIndependent_comp_of_eval, GoodProducts.equiv_toFun_eq_eval, GoodProducts.span_sum, GoodProducts.injective_sum_to, GoodProducts.good_lt_maxProducts, GoodProducts.union_succ, GoodProducts.linearIndependent_iff_sum, GoodProducts.square_commutes, GoodProducts.maxToGood_injective, GoodProducts.sum_equiv_comp_eval_eq_elim
P 📖	MathDef	2 math math: GoodProducts.P0, GoodProducts.linearIndependentAux
Proj 📖	CompOp	7 math math: proj_eq_self, ProjRestrict_coe, C0_projOrd, C1_projOrd, proj_comp_of_subset, ProjRestricts_coe, continuous_proj
ProjRestrict 📖	CompOp	7 math math: projRestricts_comp_projRestrict, coe_πs, fin_comap_jointlySurjective, ProjRestrict_coe, continuous_projRestrict, πs_apply_apply, Products.evalFacProp
ProjRestricts 📖	CompOp	9 math math: projRestricts_comp_projRestrict, πs'_apply_apply, Products.evalFacProps, projRestricts_eq_id, projRestricts_eq_comp, ProjRestricts_coe, continuous_projRestricts, coe_πs', surjective_projRestricts
contained 📖	MathDef	3 math math: contained_C1, contained_proj, contained_C'
e 📖	CompOp	4 math math: e_mem_of_eq_true, GoodProducts.finsuppSum_mem_span_eval, Products.evalCons, one_sub_e_mem_of_false
iso_map 📖	CompOp	2 math math: iso_map_bijective, spanFunctorIsoIndexFunctor_inv_app
ord 📖	CompOp	33 math math: GoodProducts.sum_to_range, injective_πs', coe_πs, Products.limitOrdinal, ord_term_aux, GoodProducts.span_sum, term_ord_aux, ord_term, succ_exact, GoodProducts.smaller_factorization, πs'_apply_apply, contained_eq_proj, GoodProducts.injective_sum_to, GoodProducts.good_lt_maxProducts, GoodProducts.union_succ, GoodProducts.linearIndependent_iff_smaller, GoodProducts.linearIndependent_iff_sum, C0_projOrd, C1_projOrd, πs_apply_apply, GoodProducts.square_commutes, contained_C1, isClosed_proj, swapTrue_mem_C1, contained_proj, GoodProducts.sum_equiv_comp_eval_eq_elim, CC_comp_zero, CC_exact, Products.prop_of_isGood_of_contained, injective_πs, coe_πs', GoodProducts.range_equiv_smaller_toFun_bijective, succ_mono
spanCone 📖	CompOp	—
spanCone_isLimit 📖	CompOp	—
spanFunctor 📖	CompOp	2 math math: spanFunctorIsoIndexFunctor_hom_app_hom_hom_apply_coe, spanFunctorIsoIndexFunctor_inv_app
spanFunctorIsoIndexFunctor 📖	CompOp	2 math math: spanFunctorIsoIndexFunctor_hom_app_hom_hom_apply_coe, spanFunctorIsoIndexFunctor_inv_app
term 📖	CompOp	8 math, 1 bridge math: ord_term_aux, term_ord_aux, ord_term, mem_C'_eq_false, GoodProducts.chain'_cons_of_lt, GoodProducts.max_eq_o_cons_tail, GoodProducts.isChain_cons_of_lt, GoodProducts.head!_eq_o_of_maxProducts bridge: swapTrue_eq_true
π 📖	CompOp	52 math math: GoodProducts.sum_to_range, projRestricts_comp_projRestrict, injective_πs', coe_πs, Products.limitOrdinal, Products.eval_πs, spanFunctorIsoIndexFunctor_hom_app_hom_hom_apply_coe, Products.eval_πs', GoodProducts.span_sum, fin_comap_jointlySurjective, GoodProducts.spanFin, succ_exact, GoodProducts.smaller_factorization, πs'_apply_apply, Products.evalFacProps, projRestricts_eq_id, contained_eq_proj, ProjRestrict_coe, GoodProducts.injective_sum_to, iso_map_bijective, GoodProducts.good_lt_maxProducts, GoodProducts.union_succ, projRestricts_eq_comp, Products.eval_πs_image', factors_prod_eq_basis_of_ne, continuous_projRestrict, GoodProducts.linearIndependent_iff_smaller, proj_eq_of_subset, GoodProducts.linearIndependent_iff_sum, πs_apply_apply, GoodProducts.finsuppSum_mem_span_eval, GoodProducts.square_commutes, spanFinBasis.span, contained_C1, isClosed_proj, ProjRestricts_coe, swapTrue_mem_C1, continuous_projRestricts, contained_proj, proj_prop_eq_self, GoodProducts.sum_equiv_comp_eval_eq_elim, CC_comp_zero, Products.evalFacProp, CC_exact, injective_πs, coe_πs', GoodProducts.range_equiv_smaller_toFun_bijective, Products.eval_πs_image, factors_prod_eq_basis, factors_prod_eq_basis_of_eq, surjective_projRestricts, succ_mono
πs 📖	CompOp	11 math math: coe_πs, Products.eval_πs, succ_exact, GoodProducts.smaller_factorization, πs_apply_apply, GoodProducts.square_commutes, CC_comp_zero, CC_exact, injective_πs, Products.eval_πs_image, succ_mono
πs' 📖	CompOp	5 math math: injective_πs', Products.eval_πs', πs'_apply_apply, Products.eval_πs_image', coe_πs'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ProjRestrict_coe 📖	mathematical	—	Set Set.instMembership π ProjRestrict Proj	—	—
ProjRestricts_coe 📖	mathematical	—	Set Set.instMembership π ProjRestricts Proj	—	—
coe_πs 📖	mathematical	—	DFunLike.coe LocallyConstant Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool LocallyConstant.instFunLike LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring π Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder ord LinearOrder.toDecidableLT Ordinal.instLinearOrder LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup LinearMap.instFunLike πs ProjRestrict	—	—
coe_πs' 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder	LocallyConstant.toFun Set.Elem π Preorder.toLT ord LinearOrder.toDecidableLT Ordinal.instLinearOrder instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool DFunLike.coe LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring LocallyConstant LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup LinearMap.instFunLike πs' ProjRestricts lt_of_lt_of_le	—	—
contained_eq_proj 📖	mathematical	contained	π Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder ord LinearOrder.toDecidableLT Ordinal.instLinearOrder	—	proj_prop_eq_self
contained_proj 📖	mathematical	—	contained π Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder ord LinearOrder.toDecidableLT Ordinal.instLinearOrder	—	—
continuous_proj 📖	mathematical	—	Continuous Pi.topologicalSpace instTopologicalSpaceBool Proj	—	continuous_pi continuous_const continuous_apply
continuous_projRestrict 📖	mathematical	—	Continuous Set.Elem π instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool ProjRestrict	—	Continuous.restrict continuous_proj
continuous_projRestricts 📖	mathematical	—	Continuous Set.Elem π instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool ProjRestricts	—	Continuous.comp proj_eq_of_subset Homeomorph.continuous continuous_projRestrict
injective_πs 📖	mathematical	—	LocallyConstant Set.Elem π Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder ord LinearOrder.toDecidableLT Ordinal.instLinearOrder instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool DFunLike.coe LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup LinearMap.instFunLike πs	—	LocallyConstant.comap_injective continuous_projRestrict Set.surjective_mapsTo_image_restrict
injective_πs' 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder	LocallyConstant Set.Elem π Preorder.toLT ord LinearOrder.toDecidableLT Ordinal.instLinearOrder instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool DFunLike.coe LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup LinearMap.instFunLike πs'	—	LocallyConstant.comap_injective continuous_projRestricts surjective_projRestricts lt_of_lt_of_le
isClosed_proj 📖	mathematical	—	IsClosed Pi.topologicalSpace instTopologicalSpaceBool π Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder ord LinearOrder.toDecidableLT Ordinal.instLinearOrder	—	Continuous.isClosedMap Function.compactSpace Finite.compactSpace Bool.instFinite Pi.t2Space TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.DiscreteTopology.metrizableSpace instDiscreteTopologyBool continuous_proj
iso_map_bijective 📖	mathematical	—	Function.Bijective Set.Elem π Profinite.IndexFunctor.obj instTopologicalSpaceBool DFunLike.coe ContinuousMap instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace ContinuousMap.instFunLike iso_map	—	Subtype.prop
ord_term 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	ord term	—	isWellOrder_lt term_ord_aux ord_term_aux
ord_term_aux 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.type SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder isWellOrder_lt	ord term	—	isWellOrder_lt Ordinal.typein_enum
projRestricts_comp_projRestrict 📖	mathematical	—	Set.Elem π ProjRestricts ProjRestrict	—	—
projRestricts_eq_comp 📖	mathematical	—	Set.Elem π ProjRestricts	—	—
projRestricts_eq_id 📖	mathematical	—	ProjRestricts Set.Elem π	—	—
proj_comp_of_subset 📖	mathematical	—	Proj	—	—
proj_eq_of_subset 📖	mathematical	—	π	—	Set.ext proj_comp_of_subset Set.image_comp
proj_eq_self 📖	mathematical	—	Proj	—	Mathlib.Tactic.Contrapose.contrapose₂
proj_prop_eq_self 📖	mathematical	—	π	—	Set.ext proj_eq_self
spanFunctorIsoIndexFunctor_hom_app_hom_hom_apply_coe 📖	mathematical	IsCompact Pi.topologicalSpace instTopologicalSpaceBool	Set Set.instMembership Profinite.IndexFunctor.obj Finset Finset.instMembership Opposite.unop DFunLike.coe ContinuousMap Set.Elem π instTopologicalSpaceSubtype ContinuousMap.instFunLike TopCat.Hom.hom CompHausLike.toTop TotallyDisconnectedSpace TopCat.carrier TopCat.str CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder Finset.partialOrder Profinite CompHausLike.category spanFunctor Profinite.indexFunctor CategoryTheory.InducedCategory.Hom.hom CompHausLike TopCat TopCat.instCategory CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.DiscreteTopology.metrizableSpace instDiscreteTopologyBool TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete spanFunctorIsoIndexFunctor	—	TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.DiscreteTopology.metrizableSpace instDiscreteTopologyBool TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete
spanFunctorIsoIndexFunctor_inv_app 📖	mathematical	IsCompact Pi.topologicalSpace instTopologicalSpaceBool	CategoryTheory.NatTrans.app Opposite Finset CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder Finset.partialOrder Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str Profinite.indexFunctor spanFunctor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.DiscreteTopology.metrizableSpace instDiscreteTopologyBool TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete spanFunctorIsoIndexFunctor CategoryTheory.Functor.obj CompHausLike.isoOfBijective CategoryTheory.ConcreteCategory.ofHom CompHausLike ContinuousMap CompHausLike.toTop ContinuousMap.instFunLike CompHausLike.concreteCategory iso_map Finset.instMembership Opposite.unop	—	TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.DiscreteTopology.metrizableSpace instDiscreteTopologyBool TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete
surjective_projRestricts 📖	mathematical	—	Set.Elem π ProjRestricts	—	proj_eq_of_subset Homeomorph.surjective Set.surjective_mapsTo_image_restrict
term_ord_aux 📖	mathematical	—	term ord	—	isWellOrder_lt Ordinal.enum_typein
πs'_apply_apply 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder	DFunLike.coe LocallyConstant Set.Elem π Preorder.toLT ord LinearOrder.toDecidableLT Ordinal.instLinearOrder instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool LocallyConstant.instFunLike LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup LinearMap.instFunLike πs' ProjRestricts	—	—
πs_apply_apply 📖	mathematical	—	DFunLike.coe LocallyConstant Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool LocallyConstant.instFunLike LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring π Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder ord LinearOrder.toDecidableLT Ordinal.instLinearOrder LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup LinearMap.instFunLike πs ProjRestrict	—	—

Profinite.NobelingProof.GoodProducts

Definitions

Name	Category	Theorems
equiv_range 📖	CompOp	1 math math: equiv_toFun_eq_eval
eval 📖	CompOp	15 math math: linearIndependent_iff_union_smaller, injective, equiv_toFun_eq_eval, span_sum, spanFin, span, linearIndependent_iff_smaller, linearIndependent_iff_sum, linearIndependent, square_commutes, linearIndependentEmpty, span_iff_products, sum_equiv_comp_eval_eq_elim, linearIndependent_iff_range, linearIndependentSingleton
range 📖	CompOp	6 math math: equiv_toFun_eq_eval, range_equiv_factorization, smaller_factorization, range_equiv_smaller_toFun_bijective, linearIndependent_iff_range, union

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv_toFun_eq_eval 📖	mathematical	—	Equiv.toFun Set.Elem Profinite.NobelingProof.Products Profinite.NobelingProof.GoodProducts LocallyConstant instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool range equiv_range Set.rangeFactorization Profinite.NobelingProof.Products.isGood eval	—	—
injective 📖	mathematical	—	Profinite.NobelingProof.Products Profinite.NobelingProof.Products.isGood LocallyConstant Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool eval	—	Ne.lt_or_gt Submodule.subset_span
linearIndependent_iff_range 📖	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 range	—	Set.rangeFactorization_eq equiv_toFun_eq_eval linearIndependent_equiv
span_iff_products 📖	mathematical	—	Submodule LocallyConstant Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool Int.instSemiring LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Top.top Submodule.instTop Submodule.span Set.range Profinite.NobelingProof.Products Profinite.NobelingProof.Products.isGood eval Profinite.NobelingProof.Products.eval	—	le_trans Submodule.span_mono Submodule.span_le IsWellFounded.induction Profinite.NobelingProof.Products.instWellFoundedLT Submodule.subset_span

Profinite.NobelingProof.Products

Definitions

Name	Category	Theorems
eval 📖	CompOp	17 math math: span_nil_eq_top, max_eq_eval, eval_πs, eval_πs', Profinite.NobelingProof.GoodProducts.span_sum, eval_eq, evalFacProps, eval_πs_image', Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval, Profinite.NobelingProof.GoodProducts.span_iff_products, Profinite.NobelingProof.GoodProducts.sum_equiv_comp_eval_eq_elim, Profinite.NobelingProof.eval_eq_πJ, evalFacProp, evalCons, Profinite.NobelingProof.GoodProducts.max_eq_eval, eval_πs_image, Profinite.NobelingProof.GoodProducts.max_eq_eval_unapply
instLinearOrder 📖	CompOp	5 math math: eval_πs_image', lt_iff_lex_lt, lt_nil_empty, instWellFoundedLT, eval_πs_image
isGood 📖	MathDef	18 math math: Profinite.NobelingProof.GoodProducts.linearIndependent_iff_union_smaller, limitOrdinal, Profinite.NobelingProof.GoodProducts.injective, Profinite.NobelingProof.GoodProducts.equiv_toFun_eq_eval, Profinite.NobelingProof.GoodProducts.span_sum, Profinite.NobelingProof.GoodProducts.spanFin, isGood_nil, Profinite.NobelingProof.GoodProducts.span, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_smaller, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_sum, Profinite.NobelingProof.instIsEmptySubtypeProductsIsGoodEmptyCollectionSetForallBool, Profinite.NobelingProof.GoodProducts.linearIndependent, Profinite.NobelingProof.GoodProducts.square_commutes, Profinite.NobelingProof.GoodProducts.linearIndependentEmpty, Profinite.NobelingProof.GoodProducts.span_iff_products, Profinite.NobelingProof.GoodProducts.sum_equiv_comp_eval_eq_elim, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_range, Profinite.NobelingProof.GoodProducts.linearIndependentSingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
evalFacProp 📖	mathematical	—	Set.Elem Profinite.NobelingProof.π DFunLike.coe LocallyConstant instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool LocallyConstant.instFunLike eval Profinite.NobelingProof.ProjRestrict	—	eval_eq
evalFacProps 📖	mathematical	—	Set.Elem Profinite.NobelingProof.π DFunLike.coe LocallyConstant instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool LocallyConstant.instFunLike eval Profinite.NobelingProof.ProjRestricts	—	Profinite.NobelingProof.proj_eq_of_subset eval_eq Profinite.NobelingProof.ProjRestricts.eq_1 Function.comp_assoc evalFacProp
eval_eq 📖	mathematical	—	DFunLike.coe LocallyConstant Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool LocallyConstant.instFunLike eval Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	eval.eq_1 map_list_prod MonoidHom.instMonoidHomClass List.prod_eq_one Int.instNontrivial NormMulClass.toNoZeroDivisors Int.instNormMulClass Mathlib.Tactic.Push.not_forall_eq
eval_πs 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Profinite.NobelingProof.ord	DFunLike.coe LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring LocallyConstant Set.Elem Profinite.NobelingProof.π LinearOrder.toDecidableLT Ordinal.instLinearOrder instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup LinearMap.instFunLike Profinite.NobelingProof.πs eval	—	evalFacProp
eval_πs' 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder Preorder.toLT Profinite.NobelingProof.ord	DFunLike.coe LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring LocallyConstant Set.Elem Profinite.NobelingProof.π LinearOrder.toDecidableLT Ordinal.instLinearOrder instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup LinearMap.instFunLike Profinite.NobelingProof.πs' eval	—	LocallyConstant.toFun_eq_coe evalFacProps lt_of_lt_of_le
eval_πs_image 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Profinite.NobelingProof.ord	Set.image Profinite.NobelingProof.Products LocallyConstant Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool eval setOf SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder Profinite.NobelingProof.π LinearOrder.toDecidableLT Ordinal.instLinearOrder DFunLike.coe LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup LinearMap.instFunLike Profinite.NobelingProof.πs	—	Set.ext eval_πs lt_ord_of_lt
eval_πs_image' 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder Preorder.toLT Profinite.NobelingProof.ord	Set.image Profinite.NobelingProof.Products LocallyConstant Set.Elem Profinite.NobelingProof.π LinearOrder.toDecidableLT Ordinal.instLinearOrder instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace instTopologicalSpaceBool eval setOf SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder DFunLike.coe LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring LocallyConstant.instAddCommMonoid Int.instAddCommMonoid AddCommGroup.toIntModule LocallyConstant.instAddCommGroup Int.instAddCommGroup LinearMap.instFunLike Profinite.NobelingProof.πs'	—	Set.ext eval_πs' lt_ord_of_lt
head!_le_of_lt 📖	mathematical	Profinite.NobelingProof.Products Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder	Preorder.toLE	—	List.head!_le_of_lt
head_lt_ord_of_isGood 📖	mathematical	isGood Profinite.NobelingProof.π Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Profinite.NobelingProof.ord LinearOrder.toDecidableLT Ordinal.instLinearOrder	SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	prop_of_isGood List.head!_mem_self
instWellFoundedLT 📖	mathematical	—	WellFoundedLT Profinite.NobelingProof.Products Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder	—	lt_iff_lex_lt WellFoundedLT.eq_1 instIsWellFoundedChainsLex_chains
isGood_mono 📖	—	Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder isGood Profinite.NobelingProof.π Preorder.toLT Profinite.NobelingProof.ord LinearOrder.toDecidableLT Ordinal.instLinearOrder	—	—	Submodule.apply_mem_span_image_iff_mem_span RingHomSurjective.ids Profinite.NobelingProof.injective_πs' eval_πs' prop_of_isGood eval_πs_image'
lt_iff_lex_lt 📖	mathematical	—	Profinite.NobelingProof.Products Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder	—	—
lt_ord_of_lt 📖	—	Profinite.NobelingProof.Products Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder Ordinal Ordinal.partialOrder Profinite.NobelingProof.ord	—	—	List.SortedGT.lt_ord_of_lt List.IsChain.sortedGT
prop_of_isGood 📖	—	isGood Profinite.NobelingProof.π Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	LocallyConstant.ext eval_eq LocallyConstant.zero_apply Submodule.zero_mem
prop_of_isGood_of_contained 📖	mathematical	isGood Profinite.NobelingProof.contained Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ordinal Ordinal.partialOrder Profinite.NobelingProof.ord	—	LocallyConstant.ext eval_eq Mathlib.Tactic.Contrapose.contrapose₂ Subtype.prop AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass
rel_head!_of_mem 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE	—	List.Pairwise.head!_le instReflGe List.SortedGE.pairwise List.SortedGT.sortedGE List.IsChain.sortedGT

---

← Back to Index