SigmaComparison

📁 Source: Mathlib/Topology/Category/CompHausLike/SigmaComparison.lean

Statistics

Metric	Count
Definitions sigmaComparison	1
Theorems instHasPropSigma, isIsoSigmaComparison, sigmaComparison_eq_comp_isos	3
Total	4

CompHausLike

Definitions

Name	Category	Theorems
sigmaComparison 📖	CompOp	3 math math: sigmaComparison_eq_comp_isos, isIsoSigmaComparison, LocallyConstant.sigmaComparison_comp_sigmaIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasPropSigma 📖	mathematical	CompactSpace T2Space HasProp	instTopologicalSpaceSigma	—	HasExplicitFiniteCoproducts.hasProp
isIsoSigmaComparison 📖	mathematical	CompactSpace T2Space HasProp	CategoryTheory.IsIso CategoryTheory.types CategoryTheory.Functor.obj Opposite CompHausLike CategoryTheory.Category.opposite category Opposite.op of instTopologicalSpaceSigma instCompactSpaceSigmaOfFinite Sigma.t2Space instHasPropSigma sigmaComparison	—	instCompactSpaceSigmaOfFinite Sigma.t2Space instHasPropSigma HasExplicitFiniteCoproducts.hasProp CategoryTheory.Limits.instHasProductOppositeOp instHasCoproduct CategoryTheory.Limits.Types.hasLimit CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts sigmaComparison_eq_comp_isos CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_hom
sigmaComparison_eq_comp_isos 📖	mathematical	CompactSpace T2Space HasProp	sigmaComparison CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types CategoryTheory.Functor.obj Opposite CompHausLike CategoryTheory.Category.opposite category Opposite.op CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor of finiteCoproduct.cofan HasExplicitFiniteCoproducts.hasProp CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.piObj CategoryTheory.Limits.instHasProductOppositeOp instHasCoproduct CategoryTheory.Limits.Pi.π CategoryTheory.Iso.hom CategoryTheory.Functor.mapIso CategoryTheory.Limits.opCoproductIsoProduct' finiteCoproduct.isColimit CategoryTheory.Limits.productIsProduct CategoryTheory.Limits.Types.hasLimit CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.PreservesProduct.iso CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts CategoryTheory.Limits.Types.productIso	—	CategoryTheory.types_ext instCompactSpaceSigmaOfFinite Sigma.t2Space instHasPropSigma HasExplicitFiniteCoproducts.hasProp CategoryTheory.Limits.instHasProductOppositeOp instHasCoproduct CategoryTheory.Limits.Types.hasLimit CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts CategoryTheory.Limits.Types.productIso_hom_comp_eval_apply CategoryTheory.Limits.piComparison_comp_π CategoryTheory.FunctorToTypes.map_comp_apply continuous_sigmaMk CategoryTheory.Limits.opCoproductIsoProduct_inv_comp_ι CategoryTheory.Category.assoc CategoryTheory.Limits.opCoproductIsoProduct'_comp_self CategoryTheory.Limits.IsColimit.fac

---

← Back to Index