Subcomplex

📁 Source: Mathlib/Topology/CWComplex/Classical/Subcomplex.lean

Statistics

Metric	Count
Definitions Subcomplex, instCWComplex, Subcomplex, instRelCWComplex	4
Theorems cell_def, map_def, union_closedCell, cellFrontier_eq, cellFrontier_subset_of_mem, cell_def, closedCell_eq, closedCell_subset_of_mem, disjoint_openCell_subcomplex_of_not_mem, finiteDimensional_subcomplex_of_finiteDimensional, finiteType_subcomplex_of_finiteType, finite_subcomplex_of_finite, map_def, openCell_eq, openCell_subset_of_mem, union_closedCell	16
Total	20

SSet

Definitions

Name	Category	Theorems
Subcomplex 📖	CompOp	91 math math: RelativeMorphism.image_le, Subcomplex.preimage_eq_top_iff, RelativeMorphism.botEquiv_symm_apply_map, Subcomplex.prod_top_le_unionProd, horn₃₁.desc.multicofork_π_two, ofSimplex_le_skeleton, Subcomplex.toSSetFunctor_map, iSup_subcomplexOfSimplex_prod_eq_top, finite_iSup_iff, Subcomplex.range_eq_top, horn₃₂.desc.multicofork_π_one, Subcomplex.topIso_inv_app_coe, Homotopy.h₁_assoc, iSup_skeleton, Subcomplex.preimage_min, Subcomplex.eq_top_iff_of_hasDimensionLT, Subcomplex.topIso_inv_ι, horn₃₁.desc.multicofork_pt, skeleton_le_skeletonOfMono, Subcomplex.toSSetFunctor_obj, hasDimensionLT_subcomplex_top_iff, Subcomplex.instSubsingletonHomToSSetBot, Subcomplex.eq_top_iff_contains_nonDegenerate, Subcomplex.preimage_range, Subcomplex.homOfLE_comp_assoc, Subcomplex.image_le_iff, horn₃₁.desc.multicofork_π_two_assoc, horn₃₁.desc.multicofork_π_zero_assoc, Subcomplex.image_monotone, skeleton_obj_eq_top, RelativeMorphism.le_preimage, instHasDimensionLTToSSetBotSubcomplex, Homotopy.h₀, RelativeMorphism.botEquiv_apply, mem_skeleton_obj_iff_of_nonDegenerate, skeleton_succ, Subcomplex.iSup_ofSimplex_nonDegenerate_eq_top, Subcomplex.image_top, Subcomplex.prod_le_unionProd, orderEmbeddingN_apply, face_le_horn, Subcomplex.image_preimage_le, Subcomplex.ofSimplex_le_iff, Subcomplex.le_iff_of_hasDimensionLT, Subcomplex.homOfLE_comp, Subcomplex.topIso_inv_ι_assoc, horn_eq_iSup, range_eq_iSup_sigma_ι, Subcomplex.BicartSq.isPushout, Subcomplex.prod_monotone, skeletonOfMono_zero, horn₃₂.desc.multicofork_π_zero_assoc, Homotopy.h₀_assoc, Homotopy.h₁, hasDimensionLT_iSup_iff, Subcomplex.le_iff_contains_nonDegenerate, mem_skeleton, iSup_skeletonOfMono, skeletonOfMono_obj_eq_top, iSup_range_eq_top_of_isColimit, horn₃₁.desc.multicofork_π_three_assoc, horn₃₁.desc.multicofork_π_zero, finite_subcomplex_top_iff, Subcomplex.preimage_max, Subcomplex.image_le_range, mem_skeletonOfMono_obj_iff_of_nonDegenerate, Subcomplex.prod_le_top_prod, horn₃₂.desc.multicofork_π_three, N.le_iff, boundary_eq_iSup, Subcomplex.unionProd.bicartSq, stdSimplex.face_inter_face, horn₃₂.desc.multicofork_pt, Subcomplex.range_eq_top_iff, Subcomplex.preimage_iSup, stdSimplex.face_le_face_iff, Subcomplex.top_prod_le_unionProd, N.iSup_subcomplex_eq_top, Subcomplex.topIso_hom, horn₃₂.desc.multicofork_π_zero, horn₃₂.desc.multicofork_π_three_assoc, horn₃₂.desc.multicofork_π_one_assoc, Subcomplex.prod_le_prod_top, horn₃₁.desc.multicofork_π_three, Subcomplex.image_iSup, range_eq_iSup_of_isColimit, Subcomplex.preimage_iInf, S.le_def, skeletonOfMono_succ, S.existsUnique_n, skeleton_zero

Topology.CWComplex.Subcomplex

Definitions

Name	Category	Theorems
instCWComplex 📖	CompOp	2 math math: cell_def, map_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cell_def 📖	mathematical	—	Topology.RelCWComplex.cell SetLike.coe Topology.RelCWComplex.Subcomplex Set Set.instEmptyCollection Topology.CWComplex.instRelCWComplex Topology.RelCWComplex.Subcomplex.instSetLike instCWComplex Set.Elem Topology.RelCWComplex.Subcomplex.I	—	—
map_def 📖	mathematical	—	Topology.RelCWComplex.map SetLike.coe Topology.RelCWComplex.Subcomplex Set Set.instEmptyCollection Topology.CWComplex.instRelCWComplex Topology.RelCWComplex.Subcomplex.instSetLike instCWComplex Topology.RelCWComplex.cell Set.instMembership Topology.RelCWComplex.Subcomplex.I	—	—
union_closedCell 📖	mathematical	—	Set.iUnion Set.Elem Topology.RelCWComplex.cell Set Set.instEmptyCollection Topology.CWComplex.instRelCWComplex Topology.RelCWComplex.Subcomplex.I Topology.RelCWComplex.closedCell Set.instMembership SetLike.coe Topology.RelCWComplex.Subcomplex Topology.RelCWComplex.Subcomplex.instSetLike	—	Set.empty_union Topology.RelCWComplex.Subcomplex.union_closedCell

Topology.RelCWComplex

Definitions

Name	Category	Theorems
Subcomplex 📖	CompData	63 math math: skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ, skeleton_top, Topology.CWComplex.exists_mem_openCell_of_mem_skeleton, Subcomplex.cellFrontier_subset_of_mem, Subcomplex.closedCell_subset_of_mem, Subcomplex.union, coe_skeletonLT, Topology.CWComplex.Subcomplex.coe_mk', mem_skeleton_iff, Subcomplex.coe_copy, cellFrontier_subset_skeletonLT, Topology.CWComplex.iUnion_openCell_eq_skeletonLT, Topology.CWComplex.Subcomplex.cell_def, mem_skeletonLT_iff, iUnion_openCell_eq_skeleton, Subcomplex.union_closedCell, Topology.CWComplex.mem_skeletonLT_iff, skeletonLT_mono, Subcomplex.ext_iff, Subcomplex.cellFrontier_eq, Subcomplex.openCell_subset_of_mem, cellFrontier_subset_skeleton, Topology.CWComplex.Subcomplex.union, openCell_subset_skeletonLT, closedCell_subset_skeletonLT, Subcomplex.finiteDimensional_subcomplex_of_finiteDimensional, skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier, Topology.CWComplex.Subcomplex.coe_mk'', skeleton_union_iUnion_closedCell_eq_skeleton_succ, Subcomplex.map_def, iUnion_skeletonLT_eq_complex, skeletonLT_zero_eq_base, iUnion_cellFrontier_subset_skeleton, Subcomplex.subset_complex, iUnion_cellFrontier_subset_skeletonLT, skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier, iUnion_openCell_eq_skeletonLT, Subcomplex.eq_iff, openCell_subset_skeleton, Subcomplex.base_subset, Topology.CWComplex.iUnion_openCell_eq_skeleton, Subcomplex.closed, skeleton_monotone, disjoint_skeleton_openCell, Subcomplex.closedCell_eq, Subcomplex.coe_mk'', Subcomplex.disjoint_openCell_subcomplex_of_not_mem, Subcomplex.coe_mk', iUnion_skeleton_eq_complex, Topology.CWComplex.Subcomplex.map_def, disjoint_skeletonLT_openCell, Subcomplex.finiteType_subcomplex_of_finiteType, Topology.CWComplex.skeletonLT_zero_eq_empty, skeletonLT_top, skeletonLT_monotone, Subcomplex.mem_carrier, Topology.CWComplex.Subcomplex.union_closedCell, Subcomplex.finite_subcomplex_of_finite, Subcomplex.openCell_eq, skeleton_mono, Subcomplex.cell_def, closedCell_subset_skeleton, Subcomplex.coe_eq_carrier

Topology.RelCWComplex.Subcomplex

Definitions

Name	Category	Theorems
instRelCWComplex 📖	CompOp	8 math math: cellFrontier_eq, finiteDimensional_subcomplex_of_finiteDimensional, map_def, closedCell_eq, finiteType_subcomplex_of_finiteType, finite_subcomplex_of_finite, openCell_eq, cell_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cellFrontier_eq 📖	mathematical	—	Topology.RelCWComplex.cellFrontier SetLike.coe Topology.RelCWComplex.Subcomplex instSetLike instRelCWComplex Topology.RelCWComplex.cell Set Set.instMembership I	—	—
cellFrontier_subset_of_mem 📖	mathematical	Topology.RelCWComplex.cell Set Set.instMembership I	Set Set.instHasSubset Topology.RelCWComplex.cellFrontier SetLike.coe Topology.RelCWComplex.Subcomplex instSetLike	—	HasSubset.Subset.trans Set.instIsTransSubset Topology.RelCWComplex.cellFrontier_subset_closedCell closedCell_subset_of_mem
cell_def 📖	mathematical	—	Topology.RelCWComplex.cell SetLike.coe Topology.RelCWComplex.Subcomplex instSetLike instRelCWComplex Set.Elem I	—	—
closedCell_eq 📖	mathematical	—	Topology.RelCWComplex.closedCell SetLike.coe Topology.RelCWComplex.Subcomplex instSetLike instRelCWComplex Topology.RelCWComplex.cell Set Set.instMembership I	—	—
closedCell_subset_of_mem 📖	mathematical	Topology.RelCWComplex.cell Set Set.instMembership I	Set Set.instHasSubset Topology.RelCWComplex.closedCell SetLike.coe Topology.RelCWComplex.Subcomplex instSetLike	—	Topology.RelCWComplex.closure_openCell_eq_closedCell IsClosed.closure_subset_iff closed union Set.subset_union_of_subset_right Set.subset_iUnion_of_subset Set.subset_iUnion
disjoint_openCell_subcomplex_of_not_mem 📖	mathematical	Topology.RelCWComplex.cell Set Set.instMembership I	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Topology.RelCWComplex.openCell SetLike.coe Topology.RelCWComplex.Subcomplex instSetLike	—	Topology.RelCWComplex.disjointBase Topology.RelCWComplex.disjoint_openCell_of_ne
finiteDimensional_subcomplex_of_finiteDimensional 📖	mathematical	—	Topology.RelCWComplex.FiniteDimensional SetLike.coe Topology.RelCWComplex.Subcomplex instSetLike instRelCWComplex	—	Filter.mp_mem Topology.RelCWComplex.FiniteDimensional.eventually_isEmpty_cell Filter.univ_mem'
finiteType_subcomplex_of_finiteType 📖	mathematical	—	Topology.RelCWComplex.FiniteType SetLike.coe Topology.RelCWComplex.Subcomplex instSetLike instRelCWComplex	—	Topology.RelCWComplex.FiniteType.finite_cell Subtype.finite
finite_subcomplex_of_finite 📖	mathematical	—	Topology.RelCWComplex.Finite SetLike.coe Topology.RelCWComplex.Subcomplex instSetLike instRelCWComplex	—	Topology.RelCWComplex.finite_of_finiteDimensional_finiteType finiteDimensional_subcomplex_of_finiteDimensional Topology.RelCWComplex.Finite.toFiniteDimensional finiteType_subcomplex_of_finiteType Topology.RelCWComplex.Finite.toFiniteType
map_def 📖	mathematical	—	Topology.RelCWComplex.map SetLike.coe Topology.RelCWComplex.Subcomplex instSetLike instRelCWComplex Topology.RelCWComplex.cell Set Set.instMembership I	—	—
openCell_eq 📖	mathematical	—	Topology.RelCWComplex.openCell SetLike.coe Topology.RelCWComplex.Subcomplex instSetLike instRelCWComplex Topology.RelCWComplex.cell Set Set.instMembership I	—	—
openCell_subset_of_mem 📖	mathematical	Topology.RelCWComplex.cell Set Set.instMembership I	Set Set.instHasSubset Topology.RelCWComplex.openCell SetLike.coe Topology.RelCWComplex.Subcomplex instSetLike	—	HasSubset.Subset.trans Set.instIsTransSubset Topology.RelCWComplex.openCell_subset_closedCell closedCell_subset_of_mem
union_closedCell 📖	mathematical	—	Set Set.instUnion Set.iUnion Set.Elem Topology.RelCWComplex.cell I Topology.RelCWComplex.closedCell Set.instMembership SetLike.coe Topology.RelCWComplex.Subcomplex instSetLike	—	subset_antisymm Set.instAntisymmSubset Set.union_subset base_subset Set.iUnion₂_subset closedCell_subset_of_mem union Set.union_subset_union_right Set.iUnion₂_mono Topology.RelCWComplex.openCell_subset_closedCell

---

← Back to Index