Basic

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

Statistics

Metric	Count
Definitions `CWComplex`, `mk'`, `mk''`, `cell`, `instRelCWComplex`, `map`, `RelCWComplex`, `I`, `carrier`, `copy`, `instPartialOrder`, `instSetLike`, `mk'`, `mk''`, `cell`, `cellFrontier`, `closedCell`, `map`, `openCell`, `skeleton`, `skeletonLT`, `toCWComplex`	22
Theorems `coe_mk'`, `coe_mk''`, `mk''_I`, `mk'_I`, `union`, `cellFrontier_subset_finite_closedCell`, `cellFrontier_subset_finite_openCell`, `cell_def`, `closed`, `closed'`, `continuousOn`, `continuousOn_symm`, `eq_of_eq_union_iUnion`, `exists_mem_openCell_of_mem_skeleton`, `iUnion_openCell_eq_complex`, `iUnion_openCell_eq_skeleton`, `iUnion_openCell_eq_skeletonLT`, `isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell`, `isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell`, `isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell`, `map_def`, `mapsTo`, `mapsTo'`, `mem_skeletonLT_iff`, `pairwiseDisjoint'`, `skeletonLT_zero_eq_empty`, `source_eq`, `union`, `union'`, `base_subset`, `closed`, `closed'`, `coe_copy`, `coe_eq_carrier`, `coe_mk'`, `coe_mk''`, `copy_eq`, `eq_iff`, `ext`, `ext_iff`, `mem_carrier`, `mk''_I`, `mk'_I`, `subset_complex`, `union`, `union'`, `base_subset_complex`, `cellFrontier_subset_base_union_finite_closedCell`, `cellFrontier_subset_closedCell`, `cellFrontier_subset_complex`, `cellFrontier_subset_finite_openCell`, `cellFrontier_subset_skeleton`, `cellFrontier_subset_skeletonLT`, `cellFrontier_union_openCell_eq_closedCell`, `cellFrontier_zero_eq_empty`, `closed`, `closed'`, `closedCell_subset_complex`, `closedCell_subset_skeleton`, `closedCell_subset_skeletonLT`, `closedCell_zero_eq_singleton`, `closure_openCell_eq_closedCell`, `coe_skeletonLT`, `continuousOn`, `continuousOn_symm`, `disjointBase`, `disjointBase'`, `disjoint_base_iUnion_openCell`, `disjoint_interior_base_closedCell`, `disjoint_interior_base_iUnion_closedCell`, `disjoint_openCell_of_ne`, `disjoint_skeletonLT_openCell`, `disjoint_skeleton_openCell`, `eq_of_eq_union_iUnion`, `eq_of_not_disjoint_openCell`, `iUnion_cellFrontier_subset_skeleton`, `iUnion_cellFrontier_subset_skeletonLT`, `iUnion_openCell_eq_skeleton`, `iUnion_openCell_eq_skeletonLT`, `iUnion_skeletonLT_eq_complex`, `iUnion_skeleton_eq_complex`, `isClosed`, `isClosedBase`, `isClosed_cellFrontier`, `isClosed_closedCell`, `isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell`, `isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell`, `isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell`, `isCompact_cellFrontier`, `isCompact_closedCell`, `map_zero_mem_closedCell`, `map_zero_mem_openCell`, `mapsTo`, `mem_skeletonLT_iff`, `mem_skeleton_iff`, `openCell_subset_closedCell`, `openCell_subset_complex`, `openCell_subset_skeleton`, `openCell_subset_skeletonLT`, `openCell_zero_eq_singleton`, `pairwiseDisjoint`, `pairwiseDisjoint'`, `skeletonLT_I`, `skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier`, `skeletonLT_mono`, `skeletonLT_monotone`, `skeletonLT_top`, `skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ`, `skeletonLT_zero_eq_base`, `skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier`, `skeleton_mono`, `skeleton_monotone`, `skeleton_top`, `skeleton_union_iUnion_closedCell_eq_skeleton_succ`, `source_eq`, `toCWComplex_cell`, `toCWComplex_eq`, `toCWComplex_map`, `union`, `union'`, `union_iUnion_openCell_eq_complex`	121
Total	143

Topology

Definitions

Name	Category	Theorems
`CWComplex` 📖	CompData	—
`RelCWComplex` 📖	CompData	—

Topology.CWComplex

Definitions

Name	Category	Theorems
`cell` 📖	CompOp	7 math math: `Topology.RelCWComplex.toCWComplex_cell`, `cell_def`, `mkFinite_cell`, `mkFiniteType_cell`, `union'`, `pairwiseDisjoint'`, `mapsTo'`
`instRelCWComplex` 📖	CompOp	20 math math: `exists_mem_openCell_of_mem_skeleton`, `iUnion_openCell_eq_skeletonLT`, `Subcomplex.cell_def`, `cell_def`, `mem_skeletonLT_iff`, `closed`, `Subcomplex.union`, `iUnion_openCell_eq_complex`, `cellFrontier_subset_finite_closedCell`, `finiteType_mkFiniteType`, `union`, `map_def`, `cellFrontier_subset_finite_openCell`, `iUnion_openCell_eq_skeleton`, `Subcomplex.map_def`, `skeletonLT_zero_eq_empty`, `mapsTo`, `Subcomplex.union_closedCell`, `Topology.RelCWComplex.toCWComplex_eq`, `finite_mkFinite`
`map` 📖	CompOp	10 math math: `continuousOn`, `mkFinite_map`, `union'`, `source_eq`, `pairwiseDisjoint'`, `mapsTo'`, `map_def`, `Topology.RelCWComplex.toCWComplex_map`, `continuousOn_symm`, `mkFiniteType_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cellFrontier_subset_finite_closedCell` 📖	mathematical	—	`Set` `Set.instHasSubset` `Topology.RelCWComplex.cellFrontier` `Set.instEmptyCollection` `instRelCWComplex` `Set.iUnion` `Topology.RelCWComplex.cell` `Finset` `Finset.instMembership` `Topology.RelCWComplex.closedCell`	—	`Topology.RelCWComplex.mapsTo` `Set.empty_union` `Set.mapsTo_iff_image_subset`
`cellFrontier_subset_finite_openCell` 📖	mathematical	—	`Set` `Set.instHasSubset` `Topology.RelCWComplex.cellFrontier` `Set.instEmptyCollection` `instRelCWComplex` `Set.iUnion` `Topology.RelCWComplex.cell` `Finset` `Finset.instMembership` `Topology.RelCWComplex.openCell`	—	`Set.empty_union` `Topology.RelCWComplex.cellFrontier_subset_finite_openCell`
`cell_def` 📖	mathematical	—	`Topology.RelCWComplex.cell` `Set` `Set.instEmptyCollection` `instRelCWComplex` `cell`	—	—
`closed` 📖	mathematical	`Set` `Set.instHasSubset`	`IsClosed` `Set.instInter` `Topology.RelCWComplex.closedCell` `Set.instEmptyCollection` `instRelCWComplex`	—	`Topology.RelCWComplex.closed` `Set.inter_empty` `T2Space.t1Space`
`closed'` 📖	—	`Set` `Set.instHasSubset` `IsClosed` `Set.instInter` `Set.image` `PartialEquiv.toFun` `map` `Metric.closedBall` `pseudoMetricSpacePi` `Real` `Fin.fintype` `Real.pseudoMetricSpace` `Pi.instZero` `Real.instZero` `Real.instOne`	—	—	—
`continuousOn` 📖	mathematical	—	`ContinuousOn` `Pi.topologicalSpace` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `PartialEquiv.toFun` `map` `Metric.closedBall` `pseudoMetricSpacePi` `Fin.fintype` `Pi.instZero` `Real.instZero` `Real.instOne`	—	—
`continuousOn_symm` 📖	mathematical	—	`ContinuousOn` `Pi.topologicalSpace` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `PartialEquiv.toFun` `PartialEquiv.symm` `map` `PartialEquiv.target`	—	—
`eq_of_eq_union_iUnion` 📖	—	`Set.iUnion` `Set.Elem` `Topology.RelCWComplex.cell` `Set` `Set.instEmptyCollection` `instRelCWComplex` `Topology.RelCWComplex.openCell` `Set.instMembership`	—	—	`Topology.RelCWComplex.eq_of_eq_union_iUnion` `Set.empty_union`
`exists_mem_openCell_of_mem_skeleton` 📖	mathematical	—	`Topology.RelCWComplex.Subcomplex` `Set` `Set.instEmptyCollection` `instRelCWComplex` `SetLike.instMembership` `Topology.RelCWComplex.Subcomplex.instSetLike` `Topology.RelCWComplex.skeleton` `Set.instMembership` `Topology.RelCWComplex.openCell`	—	`Topology.RelCWComplex.mem_skeleton_iff` `Set.mem_empty_iff_false`
`iUnion_openCell_eq_complex` 📖	mathematical	—	`Set.iUnion` `Topology.RelCWComplex.cell` `Set` `Set.instEmptyCollection` `instRelCWComplex` `Topology.RelCWComplex.openCell`	—	`Set.empty_union` `Topology.RelCWComplex.union_iUnion_openCell_eq_complex`
`iUnion_openCell_eq_skeleton` 📖	mathematical	—	`Set.iUnion` `ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Topology.RelCWComplex.cell` `Set` `Set.instEmptyCollection` `instRelCWComplex` `Topology.RelCWComplex.openCell` `SetLike.coe` `Topology.RelCWComplex.Subcomplex` `Topology.RelCWComplex.Subcomplex.instSetLike` `Topology.RelCWComplex.skeleton`	—	`iUnion_openCell_eq_skeletonLT`
`iUnion_openCell_eq_skeletonLT` 📖	mathematical	—	`Set.iUnion` `ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `Topology.RelCWComplex.cell` `Set` `Set.instEmptyCollection` `instRelCWComplex` `Topology.RelCWComplex.openCell` `SetLike.coe` `Topology.RelCWComplex.Subcomplex` `Topology.RelCWComplex.Subcomplex.instSetLike` `Topology.RelCWComplex.skeletonLT`	—	`Topology.RelCWComplex.iUnion_openCell_eq_skeletonLT` `Set.empty_union`
`isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell` 📖	mathematical	`IsClosed` `Set` `Set.instInter` `Topology.RelCWComplex.closedCell` `Set.instEmptyCollection` `instRelCWComplex`	`Topology.RelCWComplex.cellFrontier`	—	`Topology.RelCWComplex.isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell` `Set.inter_empty`
`isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell` 📖	—	`Set` `Set.instHasSubset` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Topology.RelCWComplex.openCell` `Set.instEmptyCollection` `instRelCWComplex` `IsClosed` `Set.instInter` `Topology.RelCWComplex.closedCell`	—	—	`Topology.RelCWComplex.isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell` `Set.inter_empty` `T2Space.t1Space`
`isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell` 📖	—	`Set` `Set.instHasSubset` `IsClosed` `Set.instInter` `Topology.RelCWComplex.openCell` `Set.instEmptyCollection` `instRelCWComplex` `Topology.RelCWComplex.closedCell`	—	—	`Topology.RelCWComplex.isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell` `Set.inter_empty` `T2Space.t1Space`
`map_def` 📖	mathematical	—	`Topology.RelCWComplex.map` `Set` `Set.instEmptyCollection` `instRelCWComplex` `map`	—	—
`mapsTo` 📖	mathematical	—	`Set.MapsTo` `PartialEquiv.toFun` `Topology.RelCWComplex.map` `Set` `Set.instEmptyCollection` `instRelCWComplex` `Metric.sphere` `pseudoMetricSpacePi` `Real` `Fin.fintype` `Real.pseudoMetricSpace` `Pi.instZero` `Real.instZero` `Real.instOne` `Set.iUnion` `Topology.RelCWComplex.cell` `Finset` `Finset.instMembership` `Set.image` `Metric.closedBall`	—	`Topology.RelCWComplex.mapsTo` `Set.empty_union`
`mapsTo'` 📖	mathematical	—	`Set.MapsTo` `PartialEquiv.toFun` `map` `Metric.sphere` `pseudoMetricSpacePi` `Real` `Fin.fintype` `Real.pseudoMetricSpace` `Pi.instZero` `Real.instZero` `Real.instOne` `Set.iUnion` `cell` `Finset` `Finset.instMembership` `Set.image` `Metric.closedBall`	—	—
`mem_skeletonLT_iff` 📖	mathematical	—	`Topology.RelCWComplex.Subcomplex` `Set` `Set.instEmptyCollection` `instRelCWComplex` `SetLike.instMembership` `Topology.RelCWComplex.Subcomplex.instSetLike` `Topology.RelCWComplex.skeletonLT` `Set.instMembership` `Topology.RelCWComplex.openCell`	—	—
`pairwiseDisjoint'` 📖	mathematical	—	`Set.PairwiseDisjoint` `Set` `cell` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.univ` `Set.image` `PartialEquiv.toFun` `map` `Metric.ball` `pseudoMetricSpacePi` `Real` `Fin.fintype` `Real.pseudoMetricSpace` `Pi.instZero` `Real.instZero` `Real.instOne`	—	—
`skeletonLT_zero_eq_empty` 📖	mathematical	—	`SetLike.coe` `Topology.RelCWComplex.Subcomplex` `Set` `Set.instEmptyCollection` `instRelCWComplex` `Topology.RelCWComplex.Subcomplex.instSetLike` `Topology.RelCWComplex.skeletonLT` `ENat` `instZeroENat`	—	`Topology.RelCWComplex.skeletonLT_zero_eq_base`
`source_eq` 📖	mathematical	—	`PartialEquiv.source` `map` `Metric.ball` `pseudoMetricSpacePi` `Real` `Fin.fintype` `Real.pseudoMetricSpace` `Pi.instZero` `Real.instZero` `Real.instOne`	—	—
`union` 📖	mathematical	—	`Set.iUnion` `Topology.RelCWComplex.cell` `Set` `Set.instEmptyCollection` `instRelCWComplex` `Topology.RelCWComplex.closedCell`	—	`Topology.RelCWComplex.union'` `Set.empty_union`
`union'` 📖	mathematical	—	`Set.iUnion` `cell` `Set.image` `PartialEquiv.toFun` `map` `Metric.closedBall` `pseudoMetricSpacePi` `Real` `Fin.fintype` `Real.pseudoMetricSpace` `Pi.instZero` `Real.instZero` `Real.instOne`	—	—

Topology.CWComplex.Subcomplex

Definitions

Name	Category	Theorems
`mk'` 📖	CompOp	2 math math: `mk'_I`, `coe_mk'`
`mk''` 📖	CompOp	2 math math: `coe_mk''`, `mk''_I`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mk'` 📖	mathematical	`Set` `Set.instHasSubset` `Topology.RelCWComplex.closedCell` `Set.instEmptyCollection` `Topology.CWComplex.instRelCWComplex` `Topology.RelCWComplex.cell` `Set.instMembership` `Set.iUnion` `Set.Elem` `Topology.RelCWComplex.openCell`	`SetLike.coe` `Topology.RelCWComplex.Subcomplex` `Topology.RelCWComplex.Subcomplex.instSetLike` `mk'`	—	—
`coe_mk''` 📖	mathematical	`Set.iUnion` `Set.Elem` `Topology.RelCWComplex.cell` `Set` `Set.instEmptyCollection` `Topology.CWComplex.instRelCWComplex` `Topology.RelCWComplex.openCell` `Set.instMembership`	`SetLike.coe` `Topology.RelCWComplex.Subcomplex` `Topology.RelCWComplex.Subcomplex.instSetLike` `mk''`	—	—
`mk''_I` 📖	mathematical	`Set.iUnion` `Set.Elem` `Topology.RelCWComplex.cell` `Set` `Set.instEmptyCollection` `Topology.CWComplex.instRelCWComplex` `Topology.RelCWComplex.openCell` `Set.instMembership`	`Topology.RelCWComplex.Subcomplex.I` `mk''`	—	—
`mk'_I` 📖	mathematical	`Set` `Set.instHasSubset` `Topology.RelCWComplex.closedCell` `Set.instEmptyCollection` `Topology.CWComplex.instRelCWComplex` `Topology.RelCWComplex.cell` `Set.instMembership` `Set.iUnion` `Set.Elem` `Topology.RelCWComplex.openCell`	`Topology.RelCWComplex.Subcomplex.I` `mk'`	—	—
`union` 📖	mathematical	—	`Set.iUnion` `Set.Elem` `Topology.RelCWComplex.cell` `Set` `Set.instEmptyCollection` `Topology.CWComplex.instRelCWComplex` `Topology.RelCWComplex.Subcomplex.I` `Topology.RelCWComplex.openCell` `Set.instMembership` `SetLike.coe` `Topology.RelCWComplex.Subcomplex` `Topology.RelCWComplex.Subcomplex.instSetLike`	—	`Topology.RelCWComplex.Subcomplex.union` `Set.empty_union`

Topology.RelCWComplex

Definitions

Name	Category	Theorems
`cell` 📖	CompOp	47 math math: `skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ`, `Subcomplex.union'`, `toCWComplex_cell`, `eq_of_not_disjoint_openCell`, `pairwiseDisjoint'`, `cellFrontier_subset_base_union_finite_closedCell`, `Subcomplex.union`, `coe_skeletonLT`, `Topology.CWComplex.iUnion_openCell_eq_skeletonLT`, `union_iUnion_openCell_eq_complex`, `Topology.CWComplex.Subcomplex.cell_def`, `union'`, `iUnion_openCell_eq_skeleton`, `Subcomplex.union_closedCell`, `Topology.CWComplex.cell_def`, `Subcomplex.cellFrontier_eq`, `Topology.CWComplex.mkFinite_cell`, `mkFinite_cell`, `Topology.CWComplex.Subcomplex.union`, `Topology.CWComplex.iUnion_openCell_eq_complex`, `Topology.CWComplex.cellFrontier_subset_finite_closedCell`, `mkFiniteType_cell`, `skeleton_union_iUnion_closedCell_eq_skeleton_succ`, `Subcomplex.map_def`, `iUnion_cellFrontier_subset_skeleton`, `FiniteType.finite_cell`, `iUnion_cellFrontier_subset_skeletonLT`, `cellFrontier_subset_finite_openCell`, `Topology.CWComplex.union`, `iUnion_openCell_eq_skeletonLT`, `finite_cells_of_finite`, `Topology.CWComplex.cellFrontier_subset_finite_openCell`, `mapsTo`, `Topology.CWComplex.iUnion_openCell_eq_skeleton`, `Subcomplex.closedCell_eq`, `FiniteDimensional.eventually_isEmpty_cell`, `Topology.CWComplex.Subcomplex.map_def`, `skeletonLT_I`, `pairwiseDisjoint`, `Topology.CWComplex.mapsTo`, `Topology.CWComplex.Subcomplex.union_closedCell`, `Subcomplex.openCell_eq`, `Subcomplex.cell_def`, `finite_iff_finite_cells`, `disjoint_base_iUnion_openCell`, `union`, `disjoint_interior_base_iUnion_closedCell`
`cellFrontier` 📖	CompOp	20 math math: `Subcomplex.cellFrontier_subset_of_mem`, `isCompact_cellFrontier`, `cellFrontier_subset_base_union_finite_closedCell`, `cellFrontier_subset_skeletonLT`, `Topology.CWComplex.isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell`, `Subcomplex.cellFrontier_eq`, `cellFrontier_subset_skeleton`, `isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell`, `skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier`, `Topology.CWComplex.cellFrontier_subset_finite_closedCell`, `iUnion_cellFrontier_subset_skeleton`, `iUnion_cellFrontier_subset_skeletonLT`, `skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier`, `cellFrontier_subset_finite_openCell`, `cellFrontier_subset_complex`, `Topology.CWComplex.cellFrontier_subset_finite_openCell`, `cellFrontier_zero_eq_empty`, `cellFrontier_subset_closedCell`, `cellFrontier_union_openCell_eq_closedCell`, `isClosed_cellFrontier`
`closedCell` 📖	CompOp	28 math math: `skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ`, `isCompact_closedCell`, `cellFrontier_subset_base_union_finite_closedCell`, `Subcomplex.closedCell_subset_of_mem`, `coe_skeletonLT`, `Subcomplex.union_closedCell`, `closed`, `Topology.CWComplex.closed`, `closedCell_subset_skeletonLT`, `skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier`, `Topology.CWComplex.cellFrontier_subset_finite_closedCell`, `skeleton_union_iUnion_closedCell_eq_skeleton_succ`, `isClosed_closedCell`, `disjoint_interior_base_closedCell`, `skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier`, `Topology.CWComplex.union`, `Subcomplex.closedCell_eq`, `closedCell_zero_eq_singleton`, `closedCell_subset_complex`, `cellFrontier_subset_closedCell`, `cellFrontier_union_openCell_eq_closedCell`, `Topology.CWComplex.Subcomplex.union_closedCell`, `openCell_subset_closedCell`, `closedCell_subset_skeleton`, `closure_openCell_eq_closedCell`, `union`, `map_zero_mem_closedCell`, `disjoint_interior_base_iUnion_closedCell`
`map` 📖	CompOp	19 math math: `continuousOn_symm`, `pairwiseDisjoint'`, `source_eq`, `continuousOn`, `union'`, `Topology.CWComplex.mkFinite_map`, `Subcomplex.map_def`, `mkFinite_map`, `map_zero_mem_openCell`, `Topology.CWComplex.map_def`, `openCell_zero_eq_singleton`, `mapsTo`, `closedCell_zero_eq_singleton`, `disjointBase'`, `mkFiniteType_map`, `Topology.CWComplex.Subcomplex.map_def`, `toCWComplex_map`, `Topology.CWComplex.mapsTo`, `map_zero_mem_closedCell`
`openCell` 📖	CompOp	32 math math: `Subcomplex.union'`, `Topology.CWComplex.exists_mem_openCell_of_mem_skeleton`, `disjoint_openCell_of_ne`, `Subcomplex.union`, `mem_skeleton_iff`, `Topology.CWComplex.iUnion_openCell_eq_skeletonLT`, `union_iUnion_openCell_eq_complex`, `mem_skeletonLT_iff`, `iUnion_openCell_eq_skeleton`, `Topology.CWComplex.mem_skeletonLT_iff`, `Subcomplex.openCell_subset_of_mem`, `Topology.CWComplex.Subcomplex.union`, `openCell_subset_skeletonLT`, `Topology.CWComplex.iUnion_openCell_eq_complex`, `map_zero_mem_openCell`, `openCell_subset_complex`, `cellFrontier_subset_finite_openCell`, `disjointBase`, `iUnion_openCell_eq_skeletonLT`, `openCell_zero_eq_singleton`, `openCell_subset_skeleton`, `Topology.CWComplex.cellFrontier_subset_finite_openCell`, `Topology.CWComplex.iUnion_openCell_eq_skeleton`, `disjoint_skeleton_openCell`, `Subcomplex.disjoint_openCell_subcomplex_of_not_mem`, `disjoint_skeletonLT_openCell`, `pairwiseDisjoint`, `cellFrontier_union_openCell_eq_closedCell`, `Subcomplex.openCell_eq`, `openCell_subset_closedCell`, `closure_openCell_eq_closedCell`, `disjoint_base_iUnion_openCell`
`skeleton` 📖	CompOp	15 math math: `skeleton_top`, `Topology.CWComplex.exists_mem_openCell_of_mem_skeleton`, `mem_skeleton_iff`, `iUnion_openCell_eq_skeleton`, `cellFrontier_subset_skeleton`, `skeleton_union_iUnion_closedCell_eq_skeleton_succ`, `iUnion_cellFrontier_subset_skeleton`, `skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier`, `openCell_subset_skeleton`, `Topology.CWComplex.iUnion_openCell_eq_skeleton`, `skeleton_monotone`, `disjoint_skeleton_openCell`, `iUnion_skeleton_eq_complex`, `skeleton_mono`, `closedCell_subset_skeleton`
`skeletonLT` 📖	CompOp	19 math math: `skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ`, `coe_skeletonLT`, `cellFrontier_subset_skeletonLT`, `Topology.CWComplex.iUnion_openCell_eq_skeletonLT`, `mem_skeletonLT_iff`, `Topology.CWComplex.mem_skeletonLT_iff`, `skeletonLT_mono`, `openCell_subset_skeletonLT`, `closedCell_subset_skeletonLT`, `skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier`, `iUnion_skeletonLT_eq_complex`, `skeletonLT_zero_eq_base`, `iUnion_cellFrontier_subset_skeletonLT`, `iUnion_openCell_eq_skeletonLT`, `disjoint_skeletonLT_openCell`, `Topology.CWComplex.skeletonLT_zero_eq_empty`, `skeletonLT_I`, `skeletonLT_top`, `skeletonLT_monotone`
`toCWComplex` 📖	CompOp	3 math math: `toCWComplex_cell`, `toCWComplex_map`, `toCWComplex_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`base_subset_complex` 📖	mathematical	—	`Set` `Set.instHasSubset`	—	`Set.subset_union_left`
`cellFrontier_subset_base_union_finite_closedCell` 📖	mathematical	—	`Set` `Set.instHasSubset` `cellFrontier` `Set.instUnion` `Set.iUnion` `cell` `Finset` `Finset.instMembership` `closedCell`	—	`mapsTo` `Set.mapsTo_iff_image_subset`
`cellFrontier_subset_closedCell` 📖	mathematical	—	`Set` `Set.instHasSubset` `cellFrontier` `closedCell`	—	`Set.image_mono` `Metric.sphere_subset_closedBall`
`cellFrontier_subset_complex` 📖	mathematical	—	`Set` `Set.instHasSubset` `cellFrontier`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `cellFrontier_subset_closedCell` `closedCell_subset_complex`
`cellFrontier_subset_finite_openCell` 📖	mathematical	—	`Set` `Set.instHasSubset` `cellFrontier` `Set.instUnion` `Set.iUnion` `cell` `Finset` `Finset.instMembership` `openCell`	—	`Nat.case_strong_induction_on` `cellFrontier_zero_eq_empty` `Set.iUnion_congr_Prop` `Nat.instCanonicallyOrderedAdd` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Set.union_empty` `cellFrontier_subset_base_union_finite_closedCell` `cellFrontier_union_openCell_eq_closedCell` `lt_trans`
`cellFrontier_subset_skeleton` 📖	mathematical	—	`Set` `Set.instHasSubset` `cellFrontier` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeleton` `ENat` `ENat.instNatCast`	—	`cellFrontier_subset_skeletonLT`
`cellFrontier_subset_skeletonLT` 📖	mathematical	—	`Set` `Set.instHasSubset` `cellFrontier` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeletonLT` `ENat` `ENat.instNatCast`	—	`cellFrontier_subset_base_union_finite_closedCell` `subset_trans` `Set.instIsTransSubset` `coe_skeletonLT` `Set.union_subset_union_right` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`cellFrontier_union_openCell_eq_closedCell` 📖	mathematical	—	`Set` `Set.instUnion` `cellFrontier` `openCell` `closedCell`	—	`cellFrontier.eq_1` `openCell.eq_1` `closedCell.eq_1` `Set.image_union` `Metric.sphere_union_ball`
`cellFrontier_zero_eq_empty` 📖	mathematical	—	`cellFrontier` `Set` `Set.instEmptyCollection`	—	`Matrix.zero_empty` `Metric.sphere_eq_empty_of_subsingleton` `Unique.instSubsingleton` `Fin.isEmpty'` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Set.image_empty`
`closed` 📖	mathematical	`Set` `Set.instHasSubset`	`IsClosed` `Set.instInter` `closedCell`	—	`IsClosed.inter` `isClosed_closedCell` `isClosedBase` `closed'`
`closed'` 📖	—	`Set` `Set.instHasSubset` `IsClosed` `Set.instInter` `Set.image` `PartialEquiv.toFun` `map` `Metric.closedBall` `pseudoMetricSpacePi` `Real` `Fin.fintype` `Real.pseudoMetricSpace` `Pi.instZero` `Real.instZero` `Real.instOne`	—	—	—
`closedCell_subset_complex` 📖	mathematical	—	`Set` `Set.instHasSubset` `closedCell`	—	`Set.subset_union_of_subset_right` `Set.subset_iUnion₂`
`closedCell_subset_skeleton` 📖	mathematical	—	`Set` `Set.instHasSubset` `closedCell` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeleton` `ENat` `ENat.instNatCast`	—	`closedCell_subset_skeletonLT`
`closedCell_subset_skeletonLT` 📖	mathematical	—	`Set` `Set.instHasSubset` `closedCell` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeletonLT` `ENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `ENat.instNatCast` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`coe_skeletonLT` `Nat.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Nat.instIsOrderedAddMonoid`
`closedCell_zero_eq_singleton` 📖	mathematical	—	`closedCell` `Set` `Set.instSingletonSet` `PartialEquiv.toFun` `map` `Matrix.vecEmpty` `Real`	—	`Set.image_congr` `Matrix.empty_eq` `Set.Nonempty.image_const` `Real.instZeroLEOneClass`
`closure_openCell_eq_closedCell` 📖	mathematical	—	`closure` `openCell` `closedCell`	—	`subset_antisymm` `Set.instAntisymmSubset` `IsClosed.closure_subset_iff` `isClosed_closedCell` `openCell_subset_closedCell` `closedCell.eq_1` `closure_ball` `one_ne_zero` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `ContinuousOn.image_closure` `continuousOn`
`coe_skeletonLT` 📖	mathematical	—	`SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeletonLT` `Set` `Set.instUnion` `Set.iUnion` `ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `cell` `closedCell`	—	—
`continuousOn` 📖	mathematical	—	`ContinuousOn` `Pi.topologicalSpace` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `PartialEquiv.toFun` `map` `Metric.closedBall` `pseudoMetricSpacePi` `Fin.fintype` `Pi.instZero` `Real.instZero` `Real.instOne`	—	—
`continuousOn_symm` 📖	mathematical	—	`ContinuousOn` `Pi.topologicalSpace` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `PartialEquiv.toFun` `PartialEquiv.symm` `map` `PartialEquiv.target`	—	—
`disjointBase` 📖	mathematical	—	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `openCell`	—	`disjointBase'`
`disjointBase'` 📖	mathematical	—	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.image` `PartialEquiv.toFun` `map` `Metric.ball` `pseudoMetricSpacePi` `Real` `Fin.fintype` `Real.pseudoMetricSpace` `Pi.instZero` `Real.instZero` `Real.instOne`	—	—
`disjoint_base_iUnion_openCell` 📖	mathematical	—	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.iUnion` `cell` `openCell`	—	`Set.inter_iUnion` `Set.inter_comm` `Disjoint.inter_eq` `disjointBase`
`disjoint_interior_base_closedCell` 📖	mathematical	—	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `interior` `closedCell`	—	`Set.disjoint_iff_inter_eq_empty` `closure_inter_open_nonempty_iff` `isOpen_interior` `Set.inter_comm` `closure_openCell_eq_closedCell` `Subcomplex.base_subset` `interior_subset` `Disjoint.inter_eq` `disjoint_skeletonLT_openCell` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`disjoint_interior_base_iUnion_closedCell` 📖	mathematical	—	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `interior` `Set.iUnion` `cell` `closedCell`	—	`Set.inter_iUnion` `Disjoint.inter_eq` `disjoint_interior_base_closedCell` `Set.iUnion_empty`
`disjoint_openCell_of_ne` 📖	mathematical	—	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `openCell`	—	`pairwiseDisjoint` `Set.mem_univ`
`disjoint_skeletonLT_openCell` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeletonLT` `openCell`	—	`Disjoint.symm` `disjointBase` `disjoint_openCell_of_ne` `lt_self_iff_false` `ENat.coe_lt_coe` `LT.lt.trans_le`
`disjoint_skeleton_openCell` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeleton` `openCell`	—	`disjoint_skeletonLT_openCell` `Order.add_one_le_of_lt`
`eq_of_eq_union_iUnion` 📖	—	`Set` `Set.instUnion` `Set.iUnion` `Set.Elem` `cell` `openCell` `Set.instMembership`	—	—	`Set.ext`
`eq_of_not_disjoint_openCell` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `openCell`	`cell`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `disjoint_openCell_of_ne`
`iUnion_cellFrontier_subset_skeleton` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.iUnion` `cell` `cellFrontier` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeleton` `ENat` `ENat.instNatCast`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `iUnion_cellFrontier_subset_skeletonLT` `skeletonLT_mono` `le_self_add`
`iUnion_cellFrontier_subset_skeletonLT` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.iUnion` `cell` `cellFrontier` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeletonLT` `ENat` `ENat.instNatCast`	—	`Set.iUnion_subset` `cellFrontier_subset_skeletonLT`
`iUnion_openCell_eq_skeleton` 📖	mathematical	—	`Set` `Set.instUnion` `Set.iUnion` `ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `cell` `openCell` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeleton`	—	`iUnion_openCell_eq_skeletonLT`
`iUnion_openCell_eq_skeletonLT` 📖	mathematical	—	`Set` `Set.instUnion` `Set.iUnion` `ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `cell` `openCell` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeletonLT`	—	`coe_skeletonLT`
`iUnion_skeletonLT_eq_complex` 📖	mathematical	—	`Set.iUnion` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeletonLT` `ENat` `ENat.instNatCast`	—	`subset_antisymm` `Set.instAntisymmSubset` `Set.iUnion_subset_iff` `Subcomplex.subset_complex` `Set.subset_iUnion_of_subset` `Subcomplex.base_subset` `openCell_subset_skeletonLT`
`iUnion_skeleton_eq_complex` 📖	mathematical	—	`Set.iUnion` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeleton` `ENat` `ENat.instNatCast`	—	`subset_antisymm` `Set.instAntisymmSubset` `Set.iUnion_subset_iff` `Subcomplex.subset_complex` `Set.subset_iUnion_of_subset` `Subcomplex.base_subset` `openCell_subset_skeleton`
`isClosed` 📖	mathematical	—	`IsClosed`	—	`closed` `subset_refl` `Set.instReflSubset` `Set.inter_eq_right` `closedCell_subset_complex` `isClosed_closedCell` `base_subset_complex` `isClosedBase`
`isClosedBase` 📖	mathematical	—	`IsClosed`	—	—
`isClosed_cellFrontier` 📖	mathematical	—	`IsClosed` `cellFrontier`	—	`IsCompact.isClosed` `isCompact_cellFrontier`
`isClosed_closedCell` 📖	mathematical	—	`IsClosed` `closedCell`	—	`IsCompact.isClosed` `isCompact_closedCell`
`isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell` 📖	mathematical	`IsClosed` `Set` `Set.instInter` `closedCell`	`cellFrontier`	—	`cellFrontier_subset_base_union_finite_closedCell` `Set.inter_eq_right` `Set.inter_assoc` `IsClosed.inter` `Set.inter_union_distrib_left` `Set.inter_iUnion` `Set.iUnion_congr_Prop` `Set.iUnion_subtype` `IsClosed.union` `isClosed_iUnion_of_finite` `instFiniteSubtypeLtOfLocallyFiniteOrderBot` `Finite.of_fintype` `isClosed_cellFrontier`
`isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell` 📖	—	`Set` `Set.instHasSubset` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `openCell` `IsClosed` `Set.instInter` `closedCell`	—	—	`isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell` `Set.disjoint_iff_inter_eq_empty` `isClosed_empty`
`isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell` 📖	—	`Set` `Set.instHasSubset` `IsClosed` `Set.instInter` `openCell` `closedCell`	—	—	`closed` `Nat.case_strong_induction_on` `closedCell_zero_eq_singleton` `isClosed_inter_singleton` `T2Space.t1Space` `cellFrontier_union_openCell_eq_closedCell` `Set.inter_union_distrib_left` `IsClosed.union` `isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell`
`isCompact_cellFrontier` 📖	mathematical	—	`IsCompact` `cellFrontier`	—	`IsCompact.image_of_continuousOn` `isCompact_sphere` `pi_properSpace` `instProperSpaceReal` `ContinuousOn.mono` `continuousOn` `Metric.sphere_subset_closedBall`
`isCompact_closedCell` 📖	mathematical	—	`IsCompact` `closedCell`	—	`IsCompact.image_of_continuousOn` `ProperSpace.isCompact_closedBall` `pi_properSpace` `instProperSpaceReal` `continuousOn`
`map_zero_mem_closedCell` 📖	mathematical	—	`Set` `Set.instMembership` `closedCell` `PartialEquiv.toFun` `map` `Pi.instZero` `Real` `Real.instZero`	—	`openCell_subset_closedCell` `map_zero_mem_openCell`
`map_zero_mem_openCell` 📖	mathematical	—	`Set` `Set.instMembership` `openCell` `PartialEquiv.toFun` `map` `Pi.instZero` `Real` `Real.instZero`	—	`Set.mem_image_of_mem` `dist_self` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`
`mapsTo` 📖	mathematical	—	`Set.MapsTo` `PartialEquiv.toFun` `map` `Metric.sphere` `pseudoMetricSpacePi` `Real` `Fin.fintype` `Real.pseudoMetricSpace` `Pi.instZero` `Real.instZero` `Real.instOne` `Set` `Set.instUnion` `Set.iUnion` `cell` `Finset` `Finset.instMembership` `Set.image` `Metric.closedBall`	—	—
`mem_skeletonLT_iff` 📖	mathematical	—	`Subcomplex` `SetLike.instMembership` `Subcomplex.instSetLike` `skeletonLT` `Set` `Set.instMembership` `openCell`	—	—
`mem_skeleton_iff` 📖	mathematical	—	`Subcomplex` `SetLike.instMembership` `Subcomplex.instSetLike` `skeleton` `Set` `Set.instMembership` `openCell`	—	`skeleton.eq_1` `mem_skeletonLT_iff` `top_add` `Nat.cast_one` `Nat.cast_add` `Nat.cast_lt` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `Nat.cast_le` `Order.lt_add_one_iff` `Nat.instNoMaxOrder`
`openCell_subset_closedCell` 📖	mathematical	—	`Set` `Set.instHasSubset` `openCell` `closedCell`	—	`Set.image_mono` `Metric.ball_subset_closedBall`
`openCell_subset_complex` 📖	mathematical	—	`Set` `Set.instHasSubset` `openCell`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `openCell_subset_closedCell` `closedCell_subset_complex`
`openCell_subset_skeleton` 📖	mathematical	—	`Set` `Set.instHasSubset` `openCell` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeleton` `ENat` `ENat.instNatCast`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `openCell_subset_closedCell` `closedCell_subset_skeleton`
`openCell_subset_skeletonLT` 📖	mathematical	—	`Set` `Set.instHasSubset` `openCell` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeletonLT` `ENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `ENat.instNatCast` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `openCell_subset_closedCell` `closedCell_subset_skeletonLT`
`openCell_zero_eq_singleton` 📖	mathematical	—	`openCell` `Set` `Set.instSingletonSet` `PartialEquiv.toFun` `map` `Matrix.vecEmpty` `Real`	—	`Set.image_congr` `Matrix.empty_eq` `Set.Nonempty.image_const` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`
`pairwiseDisjoint` 📖	mathematical	—	`Set.PairwiseDisjoint` `Set` `cell` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.univ` `openCell`	—	`pairwiseDisjoint'`
`pairwiseDisjoint'` 📖	mathematical	—	`Set.PairwiseDisjoint` `Set` `cell` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.univ` `Set.image` `PartialEquiv.toFun` `map` `Metric.ball` `pseudoMetricSpacePi` `Real` `Fin.fintype` `Real.pseudoMetricSpace` `Pi.instZero` `Real.instZero` `Real.instOne`	—	—
`skeletonLT_I` 📖	mathematical	—	`Subcomplex.I` `skeletonLT` `setOf` `cell` `ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast`	—	—
`skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast`	`Set` `Set.instInter` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeletonLT` `closedCell` `cellFrontier`	—	`subset_antisymm` `Set.instAntisymmSubset` `cellFrontier_union_openCell_eq_closedCell` `Set.inter_union_distrib_left` `Set.union_subset` `subset_refl` `Set.instReflSubset` `Disjoint.inter_eq` `disjoint_skeletonLT_openCell` `Set.empty_subset` `Set.inter_subset_inter_right` `cellFrontier_subset_closedCell`
`skeletonLT_mono` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat`	`Set` `Set.instHasSubset` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeletonLT`	—	`Set.union_subset_union_right` `lt_of_lt_of_le`
`skeletonLT_monotone` 📖	mathematical	—	`Monotone` `ENat` `Subcomplex` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Subcomplex.instPartialOrder` `skeletonLT`	—	`skeletonLT_mono`
`skeletonLT_top` 📖	mathematical	—	`SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeletonLT` `Top.top` `ENat` `instTopENat`	—	`Set.iUnion_congr_Prop` `Set.iUnion_true` `union`
`skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ` 📖	mathematical	—	`Set` `Set.instUnion` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeletonLT` `ENat` `ENat.instNatCast` `Set.iUnion` `cell` `closedCell` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`coe_skeletonLT` `Set.union_assoc` `Set.iUnion_congr_Prop` `Nat.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `Set.biUnion_lt_succ`
`skeletonLT_zero_eq_base` 📖	mathematical	—	`SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeletonLT` `ENat` `instZeroENat`	—	`Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Set.union_empty`
`skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast`	`Set` `Set.instInter` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeleton` `closedCell` `cellFrontier`	—	`skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier` `Order.add_one_le_of_lt`
`skeleton_mono` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat`	`Set` `Set.instHasSubset` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeleton`	—	`skeletonLT_mono` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid`
`skeleton_monotone` 📖	mathematical	—	`Monotone` `ENat` `Subcomplex` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Subcomplex.instPartialOrder` `skeleton`	—	`skeleton_mono`
`skeleton_top` 📖	mathematical	—	`SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeleton` `Top.top` `ENat` `instTopENat`	—	`skeletonLT_top`
`skeleton_union_iUnion_closedCell_eq_skeleton_succ` 📖	mathematical	—	`Set` `Set.instUnion` `SetLike.coe` `Subcomplex` `Subcomplex.instSetLike` `skeleton` `ENat` `ENat.instNatCast` `Set.iUnion` `cell` `closedCell` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ`
`source_eq` 📖	mathematical	—	`PartialEquiv.source` `map` `Metric.ball` `pseudoMetricSpacePi` `Real` `Fin.fintype` `Real.pseudoMetricSpace` `Pi.instZero` `Real.instZero` `Real.instOne`	—	—
`toCWComplex_cell` 📖	mathematical	—	`Topology.CWComplex.cell` `toCWComplex` `cell` `Set` `Set.instEmptyCollection`	—	—
`toCWComplex_eq` 📖	mathematical	—	`Topology.CWComplex.instRelCWComplex` `toCWComplex`	—	—
`toCWComplex_map` 📖	mathematical	—	`Topology.CWComplex.map` `toCWComplex` `map` `Set` `Set.instEmptyCollection`	—	—
`union` 📖	mathematical	—	`Set` `Set.instUnion` `Set.iUnion` `cell` `closedCell`	—	`union'`
`union'` 📖	mathematical	—	`Set` `Set.instUnion` `Set.iUnion` `cell` `Set.image` `PartialEquiv.toFun` `map` `Metric.closedBall` `pseudoMetricSpacePi` `Real` `Fin.fintype` `Real.pseudoMetricSpace` `Pi.instZero` `Real.instZero` `Real.instOne`	—	—
`union_iUnion_openCell_eq_complex` 📖	mathematical	—	`Set` `Set.instUnion` `Set.iUnion` `cell` `openCell`	—	`Set.iUnion_congr_Prop` `Set.iUnion_true` `union`

Topology.RelCWComplex.Subcomplex

Definitions

Name	Category	Theorems
`I` 📖	CompOp	17 math math: `union'`, `union`, `Topology.CWComplex.Subcomplex.mk'_I`, `Topology.CWComplex.Subcomplex.cell_def`, `union_closedCell`, `cellFrontier_eq`, `Topology.CWComplex.Subcomplex.union`, `mk'_I`, `map_def`, `Topology.CWComplex.Subcomplex.mk''_I`, `mk''_I`, `closedCell_eq`, `Topology.CWComplex.Subcomplex.map_def`, `Topology.RelCWComplex.skeletonLT_I`, `Topology.CWComplex.Subcomplex.union_closedCell`, `openCell_eq`, `cell_def`
`carrier` 📖	CompOp	4 math math: `union'`, `closed'`, `mem_carrier`, `coe_eq_carrier`
`copy` 📖	CompOp	2 math math: `coe_copy`, `copy_eq`
`instPartialOrder` 📖	CompOp	2 math math: `Topology.RelCWComplex.skeleton_monotone`, `Topology.RelCWComplex.skeletonLT_monotone`
`instSetLike` 📖	CompOp	60 math math: `Topology.RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ`, `Topology.RelCWComplex.skeleton_top`, `Topology.CWComplex.exists_mem_openCell_of_mem_skeleton`, `cellFrontier_subset_of_mem`, `closedCell_subset_of_mem`, `union`, `Topology.RelCWComplex.coe_skeletonLT`, `Topology.CWComplex.Subcomplex.coe_mk'`, `Topology.RelCWComplex.mem_skeleton_iff`, `Topology.RelCWComplex.cellFrontier_subset_skeletonLT`, `Topology.CWComplex.iUnion_openCell_eq_skeletonLT`, `Topology.CWComplex.Subcomplex.cell_def`, `Topology.RelCWComplex.mem_skeletonLT_iff`, `Topology.RelCWComplex.iUnion_openCell_eq_skeleton`, `union_closedCell`, `Topology.CWComplex.mem_skeletonLT_iff`, `Topology.RelCWComplex.skeletonLT_mono`, `ext_iff`, `cellFrontier_eq`, `openCell_subset_of_mem`, `Topology.RelCWComplex.cellFrontier_subset_skeleton`, `Topology.CWComplex.Subcomplex.union`, `Topology.RelCWComplex.openCell_subset_skeletonLT`, `Topology.RelCWComplex.closedCell_subset_skeletonLT`, `finiteDimensional_subcomplex_of_finiteDimensional`, `Topology.RelCWComplex.skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier`, `Topology.CWComplex.Subcomplex.coe_mk''`, `Topology.RelCWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ`, `map_def`, `Topology.RelCWComplex.iUnion_skeletonLT_eq_complex`, `Topology.RelCWComplex.skeletonLT_zero_eq_base`, `Topology.RelCWComplex.iUnion_cellFrontier_subset_skeleton`, `subset_complex`, `Topology.RelCWComplex.iUnion_cellFrontier_subset_skeletonLT`, `Topology.RelCWComplex.skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier`, `Topology.RelCWComplex.iUnion_openCell_eq_skeletonLT`, `eq_iff`, `Topology.RelCWComplex.openCell_subset_skeleton`, `base_subset`, `Topology.CWComplex.iUnion_openCell_eq_skeleton`, `closed`, `Topology.RelCWComplex.disjoint_skeleton_openCell`, `closedCell_eq`, `coe_mk''`, `disjoint_openCell_subcomplex_of_not_mem`, `coe_mk'`, `Topology.RelCWComplex.iUnion_skeleton_eq_complex`, `Topology.CWComplex.Subcomplex.map_def`, `Topology.RelCWComplex.disjoint_skeletonLT_openCell`, `finiteType_subcomplex_of_finiteType`, `Topology.CWComplex.skeletonLT_zero_eq_empty`, `Topology.RelCWComplex.skeletonLT_top`, `mem_carrier`, `Topology.CWComplex.Subcomplex.union_closedCell`, `finite_subcomplex_of_finite`, `openCell_eq`, `Topology.RelCWComplex.skeleton_mono`, `cell_def`, `Topology.RelCWComplex.closedCell_subset_skeleton`, `coe_eq_carrier`
`mk'` 📖	CompOp	2 math math: `mk'_I`, `coe_mk'`
`mk''` 📖	CompOp	2 math math: `mk''_I`, `coe_mk''`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`base_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `Topology.RelCWComplex.Subcomplex` `instSetLike`	—	`Set.subset_union_left`
`closed` 📖	mathematical	—	`IsClosed` `SetLike.coe` `Topology.RelCWComplex.Subcomplex` `instSetLike`	—	`closed'`
`closed'` 📖	mathematical	—	`IsClosed` `carrier`	—	—
`coe_copy` 📖	mathematical	`SetLike.coe` `Topology.RelCWComplex.Subcomplex` `instSetLike` `I`	`copy`	—	—
`coe_eq_carrier` 📖	mathematical	—	`SetLike.coe` `Topology.RelCWComplex.Subcomplex` `instSetLike` `carrier`	—	—
`coe_mk'` 📖	mathematical	`Set` `Set.instHasSubset` `Topology.RelCWComplex.closedCell` `Topology.RelCWComplex.cell` `Set.instMembership` `Set.instUnion` `Set.iUnion` `Set.Elem` `Topology.RelCWComplex.openCell`	`SetLike.coe` `Topology.RelCWComplex.Subcomplex` `instSetLike` `mk'`	—	—
`coe_mk''` 📖	mathematical	`Set` `Set.instUnion` `Set.iUnion` `Set.Elem` `Topology.RelCWComplex.cell` `Topology.RelCWComplex.openCell` `Set.instMembership`	`SetLike.coe` `Topology.RelCWComplex.Subcomplex` `instSetLike` `mk''`	—	—
`copy_eq` 📖	mathematical	`SetLike.coe` `Topology.RelCWComplex.Subcomplex` `instSetLike` `I`	`copy`	—	`SetLike.coe_injective`
`eq_iff` 📖	mathematical	—	`SetLike.coe` `Topology.RelCWComplex.Subcomplex` `instSetLike`	—	`SetLike.coe_injective`
`ext` 📖	—	`Topology.RelCWComplex.Subcomplex` `SetLike.instMembership` `instSetLike`	—	—	`SetLike.ext`
`ext_iff` 📖	mathematical	—	`Topology.RelCWComplex.Subcomplex` `SetLike.instMembership` `instSetLike`	—	`ext`
`mem_carrier` 📖	mathematical	—	`Set` `Set.instMembership` `carrier` `SetLike.coe` `Topology.RelCWComplex.Subcomplex` `instSetLike`	—	—
`mk''_I` 📖	mathematical	`Set` `Set.instUnion` `Set.iUnion` `Set.Elem` `Topology.RelCWComplex.cell` `Topology.RelCWComplex.openCell` `Set.instMembership`	`I` `mk''`	—	—
`mk'_I` 📖	mathematical	`Set` `Set.instHasSubset` `Topology.RelCWComplex.closedCell` `Topology.RelCWComplex.cell` `Set.instMembership` `Set.instUnion` `Set.iUnion` `Set.Elem` `Topology.RelCWComplex.openCell`	`I` `mk'`	—	—
`subset_complex` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `Topology.RelCWComplex.Subcomplex` `instSetLike`	—	`Set.union_subset_union_right` `Set.iUnion_mono` `Set.iUnion_mono'` `subset_rfl` `Set.instReflSubset`
`union` 📖	mathematical	—	`Set` `Set.instUnion` `Set.iUnion` `Set.Elem` `Topology.RelCWComplex.cell` `I` `Topology.RelCWComplex.openCell` `Set.instMembership` `SetLike.coe` `Topology.RelCWComplex.Subcomplex` `instSetLike`	—	`union'`
`union'` 📖	mathematical	—	`Set` `Set.instUnion` `Set.iUnion` `Set.Elem` `Topology.RelCWComplex.cell` `I` `Topology.RelCWComplex.openCell` `Set.instMembership` `carrier`	—	—

---

← Back to Index