FiberPartition

📁 Source: Mathlib/Topology/FiberPartition.lean

Statistics

Metric	Count
Definitions sigmaIncl, sigmaInclIncl, sigmaIsoHom	3
Theorems instCompactSpaceElemValSetMemRangeCoeLocallyConstantPreimageSingleton, instFiniteFiberCoeLocallyConstant, sigmaIsoHom_apply, sigmaIsoHom_inj, sigmaIsoHom_surj	5
Total	8

TopologicalSpace.Fiber

Definitions

Name	Category	Theorems
sigmaIncl 📖	CompOp	—
sigmaInclIncl 📖	CompOp	—
sigmaIsoHom 📖	CompOp	3 math math: sigmaIsoHom_inj, sigmaIsoHom_apply, sigmaIsoHom_surj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCompactSpaceElemValSetMemRangeCoeLocallyConstantPreimageSingleton 📖	mathematical	—	CompactSpace Set.Elem Set Set.instMembership Set.range DFunLike.coe LocallyConstant LocallyConstant.instFunLike Set.preimage Set.instSingletonSet instTopologicalSpaceSubtype	—	Subtype.prop isCompact_iff_compactSpace IsClosed.isCompact IsLocallyConstant.isClosed_fiber LocallyConstant.isLocallyConstant
instFiniteFiberCoeLocallyConstant 📖	mathematical	—	Finite Function.Fiber DFunLike.coe LocallyConstant LocallyConstant.instFunLike	—	LocallyConstant.range_finite Finite.Set.finite_range
sigmaIsoHom_apply 📖	mathematical	—	DFunLike.coe ContinuousMap Function.Fiber Set.Elem Set Set.instMembership Set.range Set.preimage Set.instSingletonSet instTopologicalSpaceSigma instTopologicalSpaceSubtype ContinuousMap.instFunLike sigmaIsoHom	—	—
sigmaIsoHom_inj 📖	mathematical	—	Function.Fiber Set.Elem Set Set.instMembership Set.range Set.preimage Set.instSingletonSet DFunLike.coe ContinuousMap instTopologicalSpaceSigma instTopologicalSpaceSubtype ContinuousMap.instFunLike sigmaIsoHom	—	Sigma.subtype_ext Set.mem_singleton_iff Set.mem_preimage
sigmaIsoHom_surj 📖	mathematical	—	Function.Fiber Set.Elem Set Set.instMembership Set.range Set.preimage Set.instSingletonSet DFunLike.coe ContinuousMap instTopologicalSpaceSigma instTopologicalSpaceSubtype ContinuousMap.instFunLike sigmaIsoHom	—	Set.mem_range_self

---

← Back to Index