Sigma

📁 Source: Mathlib/Topology/ContinuousMap/Sigma.lean

Statistics

Metric	Count
Definitions sigmaCodHomeomorph, Sigma, Sigma	3
Theorems exists_lift_sigma, isEmbedding_sigmaMk_comp, sigmaCodHomeomorph_symm_apply	3
Total	6

ContinuousMap

Definitions

Name	Category	Theorems
sigmaCodHomeomorph 📖	CompOp	1 math math: sigmaCodHomeomorph_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_lift_sigma 📖	mathematical	—	comp instTopologicalSpaceSigma sigmaMk	—	Continuous.exists_lift_sigma ContinuousMapClass.map_continuous instContinuousMapClass DFunLike.ext'
isEmbedding_sigmaMk_comp 📖	mathematical	—	Topology.IsEmbedding ContinuousMap instTopologicalSpaceSigma compactOpen comp sigmaMk	—	inducing_sigma isInducing_postcomp Topology.IsEmbedding.isInducing Topology.IsEmbedding.sigmaMk IsOpen.preimage ContinuousEvalConst.continuous_eval_const instContinuousEvalConst isOpen_sigma_fst_preimage Function.eq_of_sigmaMk_comp
sigmaCodHomeomorph_symm_apply 📖	mathematical	—	DFunLike.coe Homeomorph ContinuousMap instTopologicalSpaceSigma compactOpen EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm sigmaCodHomeomorph comp sigmaMk	—	—

FirstOrder.Language.Structure

Definitions

Name	Category	Theorems
Sigma 📖	CompOp	9 math math: FirstOrder.Language.DirectLimit.funMap_quotient_mk'_sigma_mk', FirstOrder.Language.DirectLimit.exists_quotient_mk'_sigma_mk'_eq, FirstOrder.Language.DirectLimit.funMap_equiv_unify, FirstOrder.Language.DirectLimit.relMap_quotient_mk'_sigma_mk', FirstOrder.Language.DirectLimit.equiv_iff, FirstOrder.Language.DirectLimit.lift_quotient_mk'_sigma_mk', FirstOrder.Language.DirectLimit.of_apply, FirstOrder.Language.DirectLimit.relMap_equiv_unify, FirstOrder.Language.DirectLimit.funMap_unify_equiv

MvQPF

Definitions

Name	Category	Theorems
Sigma 📖	CompOp	—

---

← Back to Index