Subcomplex

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean

Statistics

Metric	Count
Definitions eqToIso, fromPreimage, homOfLE, image, instCoeOut, instDecidableEqObjOppositeSimplexCategoryToSSet, instUniqueHomToSSetBot, isInitialBot, ofSimplex, preimage, range, toImage, toRange, toSSet, toSSetFunctor, topIso, ι	17
Theorems eqToIso_hom, eqToIso_inv, fromPreimage_app_coe, fromPreimage_ι, fromPreimage_ι_assoc, homOfLE_app_val, homOfLE_comp, homOfLE_comp_assoc, homOfLE_refl, homOfLE_ι, homOfLE_ι_assoc, image_comp, image_eq_range, image_iSup, image_id, image_le_iff, image_le_range, image_monotone, image_obj, image_ofSimplex, image_preimage_le, image_top, instEpiToImage, instEpiToRange, instIsIsoToRangeOfMono, instMonoToRange, instMonoι, instSubsingletonHomToSSetBot, lift_app_coe, lift_ι, lift_ι_assoc, mem_ofSimplex_obj, mem_ofSimplex_obj_iff, mono_homOfLE, ofSimplex_le_iff, ofSimplex_ι, preimage_eq_top_iff, preimage_iInf, preimage_iSup, preimage_max, preimage_min, preimage_obj, preimage_range, range_comp, range_eq_top, range_eq_top_iff, toImage_app_coe, toImage_ι, toImage_ι_assoc, toRange_app_val, toRange_ι, toRange_ι_assoc, toSSetFunctor_map, toSSetFunctor_obj, topIso_hom, topIso_inv_app_coe, topIso_inv_ι, topIso_inv_ι_assoc, instBalanced	59
Total	76

SSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instBalanced 📖	mathematical	—	CategoryTheory.Balanced SSet largeCategory	—	CategoryTheory.NatTrans.isIso_iff_isIso_app CategoryTheory.isIso_iff_bijective CategoryTheory.mono_iff_injective CategoryTheory.instMonoAppOfFunctor CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits CategoryTheory.Limits.Types.hasLimitsOfSize UnivLE.self CategoryTheory.epi_iff_surjective CategoryTheory.instEpiAppOfFunctor CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CategoryTheory.Limits.Types.hasColimitsOfSize

SSet.Subcomplex

Definitions

Name	Category	Theorems
eqToIso 📖	CompOp	2 math math: eqToIso_hom, eqToIso_inv
fromPreimage 📖	CompOp	3 math math: fromPreimage_ι_assoc, fromPreimage_app_coe, fromPreimage_ι
homOfLE 📖	CompOp	11 math math: toSSetFunctor_map, homOfLE_refl, eqToIso_hom, homOfLE_comp_assoc, homOfLE_ι_assoc, homOfLE_ι, homOfLE_comp, homOfLE_app_val, BicartSq.isPushout, eqToIso_inv, mono_homOfLE
image 📖	CompOp	17 math math: SSet.RelativeMorphism.image_le, toImage_ι, image_obj, image_id, toImage_ι_assoc, toImage_app_coe, instEpiToImage, image_le_iff, image_monotone, image_comp, image_top, image_preimage_le, image_eq_range, image_ofSimplex, range_comp, image_le_range, image_iSup
instCoeOut 📖	CompOp	—
instDecidableEqObjOppositeSimplexCategoryToSSet 📖	CompOp	—
instUniqueHomToSSetBot 📖	CompOp	—
isInitialBot 📖	CompOp	—
ofSimplex 📖	CompOp	28 math math: mem_ofSimplex_obj_iff, SSet.ofSimplex_le_skeleton, SSet.iSup_subcomplexOfSimplex_prod_eq_top, range_eq_ofSimplex, SSet.stdSimplex.instFiniteToSSetOfSimplex, ofSimplexProd_eq_range, SSet.stdSimplex.face_eq_ofSimplex, SSet.PtSimplex.RelStruct.δ_castSucc_map, SSet.PtSimplex.RelStruct.δ_castSucc_map_assoc, SSet.PtSimplex.MulStruct.δ_succ_succ_map_assoc, SSet.RelativeMorphism.ofSimplex₀_map, SSet.PtSimplex.MulStruct.δ_succ_succ_map, SSet.PtSimplex.MulStruct.δ_succ_castSucc_map, SSet.skeleton_succ, iSup_ofSimplex_nonDegenerate_eq_top, ofSimplex_le_iff, image_ofSimplex, SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map_assoc, mem_ofSimplex_obj, SSet.stdSimplex.ofSimplex_yonedaEquiv_δ, ofSimplex_ι, SSet.RelativeMorphism.const_map, SSet.PtSimplex.RelStruct.δ_succ_map, SSet.PtSimplex.MulStruct.δ_succ_castSucc_map_assoc, SSet.stdSimplex.face_singleton_compl, SSet.skeletonOfMono_succ, SSet.PtSimplex.RelStruct.δ_succ_map_assoc, SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map
preimage 📖	CompOp	13 math math: preimage_eq_top_iff, fromPreimage_ι_assoc, preimage_min, preimage_range, image_le_iff, SSet.RelativeMorphism.le_preimage, preimage_obj, image_preimage_le, fromPreimage_app_coe, preimage_max, preimage_iSup, fromPreimage_ι, preimage_iInf
range 📖	CompOp	25 math math: preimage_eq_top_iff, toRange_ι, SSet.instHasDimensionLTToSSetRange, range_eq_ofSimplex, range_eq_top, toRange_app_val, toRange_ι_assoc, ofSimplexProd_eq_range, SSet.stdSimplex.range_δ, preimage_range, image_top, instMonoToRange, image_eq_range, SSet.range_eq_iSup_sigma_ι, range_comp, SSet.skeletonOfMono_zero, SSet.iSup_range_eq_top_of_isColimit, image_le_range, SSet.finite_range, range_tensorHom, instEpiToRange, range_eq_top_iff, SSet.range_eq_iSup_of_isColimit, instIsIsoToRangeOfMono, SSet.skeletonOfMono_succ
toImage 📖	CompOp	4 math math: toImage_ι, toImage_ι_assoc, toImage_app_coe, instEpiToImage
toRange 📖	CompOp	6 math math: toRange_ι, toRange_app_val, toRange_ι_assoc, instMonoToRange, instEpiToRange, instIsIsoToRangeOfMono
toSSet 📖	CompOp	121 math math: lift_ι, toRange_ι, SSet.instHasDimensionLTToSSetRange, SSet.horn₃₁.desc.multicofork_π_two, SSet.horn.faceSingletonComplIso_inv_ι_assoc, SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ, fromPreimage_ι_assoc, SSet.finite_iSup_iff, SSet.horn₃₁.exists_desc, SSet.stdSimplex.instFiniteToSSetOfSimplex, toImage_ι, SSet.horn.yonedaEquiv_ι, SSet.horn₃₂.desc.multicofork_π_one, topIso_inv_app_coe, SSet.horn₃₂.ι₁_desc, homOfLE_refl, toRange_app_val, toRange_ι_assoc, hasDimensionLT_of_le, lift_ι_assoc, lift_app_coe, degenerate_eq_top_iff, toImage_ι_assoc, topIso_inv_ι, SSet.horn₃₁.ι₂_desc_assoc, instHasDimensionLTToSSet, SSet.PtSimplex.RelStruct.δ_castSucc_map, SSet.horn.faceSingletonComplIso_inv_ι, toSSetFunctor_obj, SSet.hasDimensionLT_subcomplex_top_iff, SSet.horn₃₁.ι₃_desc_assoc, instSubsingletonHomToSSetBot, SSet.instFiniteToSSet, SSet.modelCategoryQuillen.instHasLiftingPropertyιHornHAddNatOfNatOfFibration, eqToIso_hom, SSet.PtSimplex.RelStruct.δ_castSucc_map_assoc, SSet.PtSimplex.MulStruct.δ_succ_succ_map_assoc, SSet.RelativeMorphism.ofSimplex₀_map, toImage_app_coe, SSet.PtSimplex.MulStruct.δ_succ_succ_map, homOfLE_comp_assoc, instEpiToImage, SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc, SSet.horn₃₁.desc.multicofork_π_two_assoc, SSet.horn.spineId_map_hornInclusion, SSet.horn₃₁.desc.multicofork_π_zero_assoc, yonedaEquiv_coe, homOfLE_ι_assoc, SSet.RelativeMorphism.map_eq_of_mem, SSet.modelCategoryQuillen.horn_ι_mem_J, SSet.instHasDimensionLTToSSetBotSubcomplex, SSet.PtSimplex.MulStruct.δ_succ_castSucc_map, mem_nonDegenerate_iff, SSet.horn₃₂.exists_desc, SSet.stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ, SSet.horn₃₁.ι₂_desc, mem_degenerate_iff, SSet.stdSimplex.faceSingletonComplIso_hom_ι, SSet.horn₃₂.ι₃_desc, SSet.RelativeMorphism.comm_assoc, instMonoToRange, SSet.horn₃₂.ι₀_desc, homOfLE_ι, image_eq_range, SSet.RelativeMorphism.comm, SSet.horn.faceι_ι, homOfLE_comp, topIso_inv_ι_assoc, SSet.horn₂₁.isPushout, fromPreimage_app_coe, homOfLE_app_val, BicartSq.isPushout, eqToIso_inv, instMonoι, SSet.horn₃₂.ι₁_desc_assoc, SSet.horn₃₂.desc.multicofork_π_zero_assoc, SSet.horn.faceι_ι_assoc, SSet.hasDimensionLT_iSup_iff, SSet.horn.spineId_vertex_coe, SSet.horn.spineId_arrow_coe, SSet.horn₃₁.desc.multicofork_π_three_assoc, SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map_assoc, SSet.horn₃₁.desc.multicofork_π_zero, SSet.finite_subcomplex_top_iff, liftPath_arrow_coe, SSet.horn₂₀.isPushout, SSet.Quasicategory.hornFilling, SSet.finite_range, SSet.horn₃₂.desc.multicofork_π_three, SSet.horn₃₁.ι₀_desc_assoc, SSet.modelCategoryQuillen.boundary_ι_mem_I, SSet.stdSimplex.faceSingletonComplIso_hom_ι_assoc, liftPath_vertex_coe, ofSimplex_ι, mono_homOfLE, SSet.horn₂₂.isPushout, SSet.Quasicategory.hornFilling', instEpiToRange, SSet.RelativeMorphism.Homotopy.rel, SSet.stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ_assoc, fromPreimage_ι, SSet.horn₃₁.ι₃_desc, SSet.PtSimplex.RelStruct.δ_succ_map, map_ι_liftPath, topIso_hom, SSet.horn.ι_ι_assoc, SSet.horn₃₂.desc.multicofork_π_zero, SSet.horn₃₂.desc.multicofork_π_three_assoc, SSet.horn₃₂.desc.multicofork_π_one_assoc, SSet.KanComplex.hornFilling, SSet.horn.ι_ι, SSet.horn₃₁.ι₀_desc, SSet.RelativeMorphism.map_coe, SSet.PtSimplex.MulStruct.δ_succ_castSucc_map_assoc, SSet.horn₃₁.desc.multicofork_π_three, SSet.horn₃₂.ι₃_desc_assoc, SSet.horn₃₂.ι₀_desc_assoc, instIsIsoToRangeOfMono, SSet.PtSimplex.RelStruct.δ_succ_map_assoc, SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map, SSet.RelativeMorphism.Homotopy.rel_assoc
toSSetFunctor 📖	CompOp	16 math math: SSet.horn₃₁.desc.multicofork_π_two, toSSetFunctor_map, SSet.horn₃₂.desc.multicofork_π_one, SSet.horn₃₁.desc.multicofork_pt, toSSetFunctor_obj, SSet.horn₃₁.desc.multicofork_π_two_assoc, SSet.horn₃₁.desc.multicofork_π_zero_assoc, SSet.horn₃₂.desc.multicofork_π_zero_assoc, SSet.horn₃₁.desc.multicofork_π_three_assoc, SSet.horn₃₁.desc.multicofork_π_zero, SSet.horn₃₂.desc.multicofork_π_three, SSet.horn₃₂.desc.multicofork_pt, SSet.horn₃₂.desc.multicofork_π_zero, SSet.horn₃₂.desc.multicofork_π_three_assoc, SSet.horn₃₂.desc.multicofork_π_one_assoc, SSet.horn₃₁.desc.multicofork_π_three
topIso 📖	CompOp	4 math math: topIso_inv_app_coe, topIso_inv_ι, topIso_inv_ι_assoc, topIso_hom
ι 📖	CompOp	37 math math: lift_ι, toRange_ι, SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ, fromPreimage_ι_assoc, toImage_ι, toRange_ι_assoc, lift_ι_assoc, toImage_ι_assoc, SSet.modelCategoryQuillen.instHasLiftingPropertyιHornHAddNatOfNatOfFibration, SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc, SSet.horn.spineId_map_hornInclusion, yonedaEquiv_coe, homOfLE_ι_assoc, SSet.modelCategoryQuillen.horn_ι_mem_J, SSet.stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ, SSet.stdSimplex.faceSingletonComplIso_hom_ι, SSet.RelativeMorphism.comm_assoc, homOfLE_ι, image_eq_range, SSet.RelativeMorphism.comm, SSet.horn.faceι_ι, instMonoι, SSet.horn.faceι_ι_assoc, SSet.Quasicategory.hornFilling, SSet.modelCategoryQuillen.boundary_ι_mem_I, SSet.stdSimplex.faceSingletonComplIso_hom_ι_assoc, ofSimplex_ι, SSet.Quasicategory.hornFilling', SSet.RelativeMorphism.Homotopy.rel, SSet.stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ_assoc, fromPreimage_ι, map_ι_liftPath, topIso_hom, SSet.horn.ι_ι_assoc, SSet.KanComplex.hornFilling, SSet.horn.ι_ι, SSet.RelativeMorphism.Homotopy.rel_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqToIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom SSet SSet.largeCategory toSSet eqToIso homOfLE	—	—
eqToIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv SSet SSet.largeCategory toSSet eqToIso homOfLE	—	—
fromPreimage_app_coe 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Set Set.instMembership CategoryTheory.Subfunctor.obj CategoryTheory.NatTrans.app toSSet preimage fromPreimage Set.preimage	—	—
fromPreimage_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory toSSet preimage fromPreimage ι	—	—
fromPreimage_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory toSSet preimage fromPreimage ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fromPreimage_ι
homOfLE_app_val 📖	mathematical	SSet.Subcomplex Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory	CategoryTheory.Functor.obj CategoryTheory.types Set Set.instMembership CategoryTheory.Subfunctor.obj CategoryTheory.NatTrans.app toSSet homOfLE	—	—
homOfLE_comp 📖	mathematical	SSet.Subcomplex Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory toSSet homOfLE LE.le.trans	—	—
homOfLE_comp_assoc 📖	mathematical	SSet.Subcomplex Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory toSSet homOfLE LE.le.trans	—	LE.le.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homOfLE_comp
homOfLE_refl 📖	mathematical	—	homOfLE CategoryTheory.CategoryStruct.id SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory toSSet	—	—
homOfLE_ι 📖	mathematical	SSet.Subcomplex Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory toSSet homOfLE ι	—	—
homOfLE_ι_assoc 📖	mathematical	SSet.Subcomplex Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory toSSet homOfLE ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homOfLE_ι
image_comp 📖	mathematical	—	image CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory	—	CategoryTheory.Subfunctor.ext Set.ext Set.image_congr
image_eq_range 📖	mathematical	—	image range toSSet CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory ι	—	CategoryTheory.Subfunctor.ext Set.ext
image_iSup 📖	mathematical	—	image iSup SSet.Subcomplex ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory	—	CategoryTheory.Subfunctor.ext Set.ext CategoryTheory.Subfunctor.iSup_obj
image_id 📖	mathematical	—	image CategoryTheory.CategoryStruct.id SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory	—	CategoryTheory.Subfunctor.ext Set.ext Set.image_congr Set.image_id'
image_le_iff 📖	mathematical	—	SSet.Subcomplex Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory image preimage	—	—
image_le_range 📖	mathematical	—	SSet.Subcomplex Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory image range	—	preimage_range
image_monotone 📖	mathematical	—	Monotone SSet.Subcomplex PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory image	—	image_le_iff LE.le.trans le_refl
image_obj 📖	mathematical	—	CategoryTheory.Subfunctor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory image Set.image CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.NatTrans.app	—	—
image_ofSimplex 📖	mathematical	—	image ofSimplex CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op	—	le_antisymm image_le_iff ofSimplex_le_iff preimage_obj Set.mem_preimage mem_ofSimplex_obj
image_preimage_le 📖	mathematical	—	SSet.Subcomplex Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory image preimage	—	image_le_iff le_refl
image_top 📖	mathematical	—	image Top.top SSet.Subcomplex OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder range	—	CategoryTheory.Subfunctor.ext Set.ext Set.image_univ
instEpiToImage 📖	mathematical	—	CategoryTheory.Epi SSet SSet.largeCategory toSSet image toImage	—	range_eq_top_iff le_antisymm
instEpiToRange 📖	mathematical	—	CategoryTheory.Epi SSet SSet.largeCategory toSSet range toRange	—	CategoryTheory.Subfunctor.instEpiFunctorTypeToRange
instIsIsoToRangeOfMono 📖	mathematical	—	CategoryTheory.IsIso SSet SSet.largeCategory toSSet range toRange	—	CategoryTheory.isIso_of_mono_of_epi SSet.instBalanced instMonoToRange instEpiToRange
instMonoToRange 📖	mathematical	—	CategoryTheory.Mono SSet SSet.largeCategory toSSet range toRange	—	CategoryTheory.mono_of_mono_fac toRange_ι
instMonoι 📖	mathematical	—	CategoryTheory.Mono SSet SSet.largeCategory toSSet ι	—	CategoryTheory.Subfunctor.instMonoFunctorTypeι
instSubsingletonHomToSSetBot 📖	mathematical	—	Quiver.Hom SSet CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SSet.largeCategory toSSet Bot.bot SSet.Subcomplex OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	SSet.hom_ext CategoryTheory.types_ext
lift_app_coe 📖	mathematical	SSet.Subcomplex Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory range	CategoryTheory.Functor.obj CategoryTheory.types Set Set.instMembership CategoryTheory.Subfunctor.obj CategoryTheory.NatTrans.app toSSet lift	—	—
lift_ι 📖	mathematical	SSet.Subcomplex Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory range	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory toSSet lift ι	—	—
lift_ι_assoc 📖	mathematical	SSet.Subcomplex Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory range	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory toSSet lift ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_ι
mem_ofSimplex_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj ofSimplex	—	CategoryTheory.Subfunctor.mem_ofSection_obj
mem_ofSimplex_obj_iff 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Set Set.instMembership CategoryTheory.Subfunctor.obj ofSimplex CategoryTheory.Functor.map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
mono_homOfLE 📖	mathematical	SSet.Subcomplex Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory	CategoryTheory.Mono SSet SSet.largeCategory toSSet homOfLE	—	CategoryTheory.mono_of_mono_fac instMonoι homOfLE_ι
ofSimplex_le_iff 📖	mathematical	—	SSet.Subcomplex Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory ofSimplex CategoryTheory.Functor.obj CategoryTheory.types Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj	—	CategoryTheory.Subfunctor.ofSection_le_iff
ofSimplex_ι 📖	mathematical	—	ι ofSimplex SSet.const toSSet	—	SSet.hom_ext CategoryTheory.types_ext SimplexCategory.instSubsingletonHomMkOfNatNat
preimage_eq_top_iff 📖	mathematical	—	preimage Top.top SSet.Subcomplex OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.instPartialOrderSubfunctor range	—	image_top image_le_iff top_le_iff
preimage_iInf 📖	mathematical	—	preimage iInf SSet.Subcomplex ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory	—	CategoryTheory.Subfunctor.ext Set.ext CategoryTheory.Subfunctor.iInf_obj
preimage_iSup 📖	mathematical	—	preimage iSup SSet.Subcomplex ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory	—	CategoryTheory.Subfunctor.ext Set.ext CategoryTheory.Subfunctor.iSup_obj Set.preimage_iUnion
preimage_max 📖	mathematical	—	preimage SSet.Subcomplex SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory	—	—
preimage_min 📖	mathematical	—	preimage SSet.Subcomplex SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory	—	—
preimage_obj 📖	mathematical	—	CategoryTheory.Subfunctor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory preimage Set.preimage CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.NatTrans.app	—	—
preimage_range 📖	mathematical	—	preimage range Top.top SSet.Subcomplex OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	le_antisymm image_le_iff image_top le_refl
range_comp 📖	mathematical	—	range CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory image	—	CategoryTheory.Subfunctor.ext Set.ext
range_eq_top 📖	mathematical	—	range Top.top SSet.Subcomplex OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	range_eq_top_iff
range_eq_top_iff 📖	mathematical	—	range Top.top SSet.Subcomplex OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Epi SSet SSet.largeCategory	—	CategoryTheory.NatTrans.epi_iff_epi_app CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CategoryTheory.Subfunctor.ext_iff
toImage_app_coe 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Set Set.instMembership CategoryTheory.Subfunctor.obj image CategoryTheory.NatTrans.app toSSet toImage	—	—
toImage_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory toSSet image toImage ι	—	—
toImage_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory toSSet image toImage ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toImage_ι
toRange_app_val 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Set Set.instMembership CategoryTheory.Subfunctor.obj range CategoryTheory.NatTrans.app toSSet toRange	—	—
toRange_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory toSSet range toRange ι	—	—
toRange_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory toSSet range toRange ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toRange_ι
toSSetFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map SSet.Subcomplex Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory SSet SSet.largeCategory toSSetFunctor homOfLE	—	—
toSSetFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj SSet.Subcomplex Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory SSet SSet.largeCategory toSSetFunctor toSSet	—	—
topIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom SSet SSet.largeCategory toSSet Top.top SSet.Subcomplex OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder topIso ι	—	—
topIso_inv_app_coe 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Set Set.instMembership CategoryTheory.Subfunctor.obj Top.top SSet.Subcomplex OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.NatTrans.app toSSet CategoryTheory.Iso.inv SSet SSet.largeCategory topIso	—	—
topIso_inv_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory toSSet Top.top SSet.Subcomplex OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Iso.inv topIso CategoryTheory.Subfunctor.ι CategoryTheory.CategoryStruct.id	—	—
topIso_inv_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory toSSet Top.top SSet.Subcomplex OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Iso.inv topIso CategoryTheory.Subfunctor.ι	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' topIso_inv_ι

---

← Back to Index