Basic

📁 Source: Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean

Statistics

Metric	Count
Definitions `instAdd`, `instAddAction`, `instAddCommGroup`, `instAddCommMagma`, `instAddCommMonoid`, `instAddCommSemigroup`, `instAddGroup`, `instAddMonoid`, `instAddSemigroup`, `instAddZeroClass`, `instAlgebra`, `instCommGroup`, `instCommMagma`, `instCommMonoid`, `instCommMonoidWithZero`, `instCommRing`, `instCommSemigroup`, `instCommSemiring`, `instDistrib`, `instDistribMulAction`, `instDistribSMul`, `instDiv`, `instGroup`, `instHasDistribNeg`, `instIntCast`, `instInv`, `instInvOneClass`, `instInvolutiveInv`, `instInvolutiveNeg`, `instModule`, `instMonoid`, `instMonoidWithZero`, `instMul`, `instMulAction`, `instMulDistribMulAction`, `instMulOneClass`, `instMulZeroClass`, `instMulZeroOneClass`, `instNSmul`, `instNatCast`, `instNeg`, `instNegZeroClass`, `instNonAssocRing`, `instNonAssocSemiring`, `instNonUnitalCommRing`, `instNonUnitalCommSemiring`, `instNonUnitalNonAssocCommRing`, `instNonUnitalNonAssocCommSemiring`, `instNonUnitalNonAssocRing`, `instNonUnitalRing`, `instNonUnitalSemiring`, `instNonUnitalnonAssocSemiring`, `instPow`, `instRing`, `instSMul`, `instSMulZeroClass`, `instSemigroup`, `instSemigroupWithZero`, `instSemiring`, `instSub`, `instVAdd`, `instZPow`, `instZSMul`, `liftCLM`, `mkAddMonoidHom`, `mkCLM`, `mkMonoidHom`, `mkRingHom`	68
Theorems `instContinuousAdd`, `instContinuousConstSMul`, `instContinuousConstVAdd`, `instContinuousDiv`, `instContinuousInv`, `instContinuousMul`, `instContinuousNeg`, `instContinuousSMul`, `instContinuousSub`, `instIsCentralScalar`, `instIsCentralVAdd`, `instIsPretransitiveSMul`, `instIsPretransitiveVAdd`, `instIsScalarTower`, `instIsTopologicalAddGroup`, `instIsTopologicalGroup`, `instIsUniformAddGroup`, `instIsUniformGroup`, `instLeftDistribClass`, `instRightDistribClass`, `instSMulCommClass`, `instVAddAssocClass`, `instVAddCommClass`, `liftCLM_apply`, `liftCLM_mk`, `mkAddMonoidHom_apply`, `mkCLM_apply`, `mkMonoidHom_apply`, `mkRingHom_apply`, `mk_add`, `mk_algebraMap`, `mk_div`, `mk_intCast`, `mk_inv`, `mk_mul`, `mk_natCast`, `mk_neg`, `mk_nsmul`, `mk_ofNat`, `mk_pow`, `mk_smul`, `mk_sub`, `mk_vadd`, `mk_zpow`, `mk_zsmul`	45
Total	113

SeparationQuotient

Definitions

Name	Category	Theorems
`instAdd` 📖	CompOp	4 math math: `mk_add`, `instContinuousAdd`, `instRightDistribClass`, `instLeftDistribClass`
`instAddAction` 📖	CompOp	—
`instAddCommGroup` 📖	CompOp	—
`instAddCommMagma` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	14 math math: `mkCLM_comp_outCLM`, `outCLM_uniformContinuous`, `outCLM_isUniformEmbedding`, `exists_out_continuousLinearMap`, `mk_outCLM`, `postcomp_mkCLM_surjective`, `mk_comp_outCLM`, `liftCLM_apply`, `isEmbedding_outCLM`, `liftCLM_mk`, `mkCLM_apply`, `instModuleFinite`, `outCLM_injective`, `outCLM_isUniformInducing`
`instAddCommSemigroup` 📖	CompOp	—
`instAddGroup` 📖	CompOp	2 math math: `instIsUniformAddGroup`, `instIsTopologicalAddGroup`
`instAddMonoid` 📖	CompOp	2 math math: `liftContinuousAddCommMonoidHom_mk`, `liftNormedAddGroupHom_apply`
`instAddSemigroup` 📖	CompOp	—
`instAddZeroClass` 📖	CompOp	2 math math: `mkAddMonoidHom_apply`, `normedMk_apply`
`instAlgebra` 📖	CompOp	1 math math: `mk_algebraMap`
`instCommGroup` 📖	CompOp	—
`instCommMagma` 📖	CompOp	—
`instCommMonoid` 📖	CompOp	—
`instCommMonoidWithZero` 📖	CompOp	—
`instCommRing` 📖	CompOp	—
`instCommSemigroup` 📖	CompOp	—
`instCommSemiring` 📖	CompOp	—
`instDistrib` 📖	CompOp	—
`instDistribMulAction` 📖	CompOp	—
`instDistribSMul` 📖	CompOp	—
`instDiv` 📖	CompOp	2 math math: `mk_div`, `instContinuousDiv`
`instGroup` 📖	CompOp	2 math math: `instIsTopologicalGroup`, `instIsUniformGroup`
`instHasDistribNeg` 📖	CompOp	—
`instIntCast` 📖	CompOp	1 math math: `mk_intCast`
`instInv` 📖	CompOp	2 math math: `instContinuousInv`, `mk_inv`
`instInvOneClass` 📖	CompOp	—
`instInvolutiveInv` 📖	CompOp	—
`instInvolutiveNeg` 📖	CompOp	—
`instModule` 📖	CompOp	14 math math: `mkCLM_comp_outCLM`, `outCLM_uniformContinuous`, `outCLM_isUniformEmbedding`, `exists_out_continuousLinearMap`, `mk_outCLM`, `postcomp_mkCLM_surjective`, `mk_comp_outCLM`, `liftCLM_apply`, `isEmbedding_outCLM`, `liftCLM_mk`, `mkCLM_apply`, `instModuleFinite`, `outCLM_injective`, `outCLM_isUniformInducing`
`instMonoid` 📖	CompOp	1 math math: `liftContinuousCommMonoidHom_mk`
`instMonoidWithZero` 📖	CompOp	—
`instMul` 📖	CompOp	4 math math: `mk_mul`, `instContinuousMul`, `instRightDistribClass`, `instLeftDistribClass`
`instMulAction` 📖	CompOp	—
`instMulDistribMulAction` 📖	CompOp	—
`instMulOneClass` 📖	CompOp	1 math math: `mkMonoidHom_apply`
`instMulZeroClass` 📖	CompOp	—
`instMulZeroOneClass` 📖	CompOp	—
`instNSmul` 📖	CompOp	1 math math: `mk_nsmul`
`instNatCast` 📖	CompOp	2 math math: `mk_natCast`, `mk_ofNat`
`instNeg` 📖	CompOp	2 math math: `instContinuousNeg`, `mk_neg`
`instNegZeroClass` 📖	CompOp	—
`instNonAssocRing` 📖	CompOp	—
`instNonAssocSemiring` 📖	CompOp	1 math math: `mkRingHom_apply`
`instNonUnitalCommRing` 📖	CompOp	—
`instNonUnitalCommSemiring` 📖	CompOp	—
`instNonUnitalNonAssocCommRing` 📖	CompOp	—
`instNonUnitalNonAssocCommSemiring` 📖	CompOp	—
`instNonUnitalNonAssocRing` 📖	CompOp	—
`instNonUnitalRing` 📖	CompOp	—
`instNonUnitalSemiring` 📖	CompOp	—
`instNonUnitalnonAssocSemiring` 📖	CompOp	—
`instPow` 📖	CompOp	1 math math: `mk_pow`
`instRing` 📖	CompOp	—
`instSMul` 📖	CompOp	8 math math: `mk_smul`, `instIsScalarTower`, `instIsBoundedSMulSeparationQuotient`, `instIsCentralScalar`, `instIsPretransitiveSMul`, `instContinuousConstSMul`, `instSMulCommClass`, `instContinuousSMul`
`instSMulZeroClass` 📖	CompOp	—
`instSemigroup` 📖	CompOp	—
`instSemigroupWithZero` 📖	CompOp	—
`instSemiring` 📖	CompOp	1 math math: `mk_algebraMap`
`instSub` 📖	CompOp	2 math math: `mk_sub`, `instContinuousSub`
`instVAdd` 📖	CompOp	6 math math: `instIsPretransitiveVAdd`, `instIsCentralVAdd`, `mk_vadd`, `instVAddCommClass`, `instVAddAssocClass`, `instContinuousConstVAdd`
`instZPow` 📖	CompOp	1 math math: `mk_zpow`
`instZSMul` 📖	CompOp	1 math math: `mk_zsmul`
`liftCLM` 📖	CompOp	2 math math: `liftCLM_apply`, `liftCLM_mk`
`mkAddMonoidHom` 📖	CompOp	2 math math: `mkAddMonoidHom_apply`, `normedMk_apply`
`mkCLM` 📖	CompOp	4 math math: `mkCLM_comp_outCLM`, `exists_out_continuousLinearMap`, `postcomp_mkCLM_surjective`, `mkCLM_apply`
`mkMonoidHom` 📖	CompOp	1 math math: `mkMonoidHom_apply`
`mkRingHom` 📖	CompOp	1 math math: `mkRingHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instContinuousAdd` 📖	mathematical	—	`ContinuousAdd` `SeparationQuotient` `instTopologicalSpaceSeparationQuotient` `instAdd`	—	`Topology.IsQuotientMap.continuous_iff` `Continuous.comp` `continuous_add`
`instContinuousConstSMul` 📖	mathematical	—	`ContinuousConstSMul` `SeparationQuotient` `instTopologicalSpaceSeparationQuotient` `instSMul`	—	`Topology.IsQuotientMap.continuous_iff` `Continuous.comp` `ContinuousConstSMul.continuous_const_smul`
`instContinuousConstVAdd` 📖	mathematical	—	`ContinuousConstVAdd` `SeparationQuotient` `instTopologicalSpaceSeparationQuotient` `instVAdd`	—	`Topology.IsQuotientMap.continuous_iff` `Continuous.comp` `ContinuousConstVAdd.continuous_const_vadd`
`instContinuousDiv` 📖	mathematical	—	`ContinuousDiv` `SeparationQuotient` `instTopologicalSpaceSeparationQuotient` `instDiv`	—	`Topology.IsQuotientMap.continuous_iff` `Continuous.comp` `ContinuousDiv.continuous_div'`
`instContinuousInv` 📖	mathematical	—	`ContinuousInv` `SeparationQuotient` `instTopologicalSpaceSeparationQuotient` `instInv`	—	`Topology.IsQuotientMap.continuous_iff` `Continuous.comp` `ContinuousInv.continuous_inv`
`instContinuousMul` 📖	mathematical	—	`ContinuousMul` `SeparationQuotient` `instTopologicalSpaceSeparationQuotient` `instMul`	—	`Topology.IsQuotientMap.continuous_iff` `Continuous.comp` `continuous_mul`
`instContinuousNeg` 📖	mathematical	—	`ContinuousNeg` `SeparationQuotient` `instTopologicalSpaceSeparationQuotient` `instNeg`	—	`Topology.IsQuotientMap.continuous_iff` `Continuous.comp` `ContinuousNeg.continuous_neg`
`instContinuousSMul` 📖	mathematical	—	`ContinuousSMul` `SeparationQuotient` `instSMul` `ContinuousSMul.continuousConstSMul` `instTopologicalSpaceSeparationQuotient`	—	`ContinuousSMul.continuousConstSMul` `Topology.IsQuotientMap.continuous_iff` `IsOpenQuotientMap.isQuotientMap` `IsOpenQuotientMap.prodMap` `IsOpenQuotientMap.id` `Continuous.comp` `ContinuousSMul.continuous_smul`
`instContinuousSub` 📖	mathematical	—	`ContinuousSub` `SeparationQuotient` `instTopologicalSpaceSeparationQuotient` `instSub`	—	`Topology.IsQuotientMap.continuous_iff` `Continuous.comp` `ContinuousSub.continuous_sub`
`instIsCentralScalar` 📖	mathematical	—	`IsCentralScalar` `SeparationQuotient` `instSMul` `MulOpposite` `ContinuousConstSMul.op`	—	`ContinuousConstSMul.op` `Function.Surjective.forall` `IsCentralScalar.op_smul_eq_smul`
`instIsCentralVAdd` 📖	mathematical	—	`IsCentralVAdd` `SeparationQuotient` `instVAdd` `AddOpposite` `ContinuousConstVAdd.op`	—	`ContinuousConstVAdd.op` `Function.Surjective.forall` `IsCentralVAdd.op_vadd_eq_vadd`
`instIsPretransitiveSMul` 📖	mathematical	—	`MulAction.IsPretransitive` `SeparationQuotient` `instSMul`	—	`Function.Surjective.forall₂` `MulAction.exists_smul_eq`
`instIsPretransitiveVAdd` 📖	mathematical	—	`AddAction.IsPretransitive` `SeparationQuotient` `instVAdd`	—	`Function.Surjective.forall₂` `AddAction.exists_vadd_eq`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `SeparationQuotient` `instSMul`	—	`Function.Surjective.forall` `smul_assoc`
`instIsTopologicalAddGroup` 📖	mathematical	—	`IsTopologicalAddGroup` `SeparationQuotient` `instTopologicalSpaceSeparationQuotient` `instAddGroup`	—	`instContinuousAdd` `IsTopologicalAddGroup.toContinuousAdd` `instContinuousNeg` `IsTopologicalAddGroup.toContinuousNeg`
`instIsTopologicalGroup` 📖	mathematical	—	`IsTopologicalGroup` `SeparationQuotient` `instTopologicalSpaceSeparationQuotient` `instGroup`	—	`instContinuousMul` `IsTopologicalGroup.toContinuousMul` `instContinuousInv` `IsTopologicalGroup.toContinuousInv`
`instIsUniformAddGroup` 📖	mathematical	—	`IsUniformAddGroup` `SeparationQuotient` `UniformSpace.toTopologicalSpace` `instUniformSpace` `instAddGroup` `IsUniformAddGroup.to_topologicalAddGroup`	—	`IsUniformAddGroup.to_topologicalAddGroup` `uniformContinuous_dom₂` `UniformContinuous.comp` `uniformContinuous_sub`
`instIsUniformGroup` 📖	mathematical	—	`IsUniformGroup` `SeparationQuotient` `UniformSpace.toTopologicalSpace` `instUniformSpace` `instGroup` `IsUniformGroup.to_topologicalGroup`	—	`IsUniformGroup.to_topologicalGroup` `uniformContinuous_dom₂` `UniformContinuous.comp` `uniformContinuous_div`
`instLeftDistribClass` 📖	mathematical	—	`LeftDistribClass` `SeparationQuotient` `instMul` `instAdd`	—	`Function.Surjective.leftDistribClass` `mk_add` `mk_mul`
`instRightDistribClass` 📖	mathematical	—	`RightDistribClass` `SeparationQuotient` `instMul` `instAdd`	—	`Function.Surjective.rightDistribClass` `mk_add` `mk_mul`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `SeparationQuotient` `instSMul`	—	`Function.Surjective.smulCommClass` `mk_smul`
`instVAddAssocClass` 📖	mathematical	—	`VAddAssocClass` `SeparationQuotient` `instVAdd`	—	`Function.Surjective.forall` `vadd_assoc`
`instVAddCommClass` 📖	mathematical	—	`VAddCommClass` `SeparationQuotient` `instVAdd`	—	`Function.Surjective.vaddCommClass` `mk_vadd`
`liftCLM_apply` 📖	mathematical	`DFunLike.coe` `ContinuousLinearMap` `ContinuousLinearMap.funLike`	`SeparationQuotient` `instTopologicalSpaceSeparationQuotient` `instAddCommMonoid` `instModule` `liftCLM` `lift`	—	—
`liftCLM_mk` 📖	mathematical	`DFunLike.coe` `ContinuousLinearMap` `ContinuousLinearMap.funLike`	`SeparationQuotient` `instTopologicalSpaceSeparationQuotient` `instAddCommMonoid` `instModule` `liftCLM`	—	—
`mkAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `SeparationQuotient` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoidHom.instFunLike` `mkAddMonoidHom`	—	—
`mkCLM_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeparationQuotient` `instTopologicalSpaceSeparationQuotient` `instAddCommMonoid` `instModule` `ContinuousLinearMap.funLike` `mkCLM`	—	—
`mkMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `SeparationQuotient` `MulOneClass.toMulOne` `instMulOneClass` `MonoidHom.instFunLike` `mkMonoidHom`	—	—
`mkRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `SeparationQuotient` `instNonAssocSemiring` `RingHom.instFunLike` `mkRingHom`	—	—
`mk_add` 📖	mathematical	—	`SeparationQuotient` `instAdd`	—	—
`mk_algebraMap` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `SeparationQuotient` `instSemiring` `instAlgebra`	—	—
`mk_div` 📖	mathematical	—	`SeparationQuotient` `instDiv`	—	—
`mk_intCast` 📖	mathematical	—	`SeparationQuotient` `instIntCast`	—	—
`mk_inv` 📖	mathematical	—	`SeparationQuotient` `instInv`	—	—
`mk_mul` 📖	mathematical	—	`SeparationQuotient` `instMul`	—	—
`mk_natCast` 📖	mathematical	—	`SeparationQuotient` `instNatCast`	—	—
`mk_neg` 📖	mathematical	—	`SeparationQuotient` `instNeg`	—	—
`mk_nsmul` 📖	mathematical	—	`AddMonoid.toNatSMul` `SeparationQuotient` `instNSmul`	—	—
`mk_ofNat` 📖	mathematical	—	`SeparationQuotient` `instOfNatAtLeastTwo` `instNatCast`	—	—
`mk_pow` 📖	mathematical	—	`Monoid.toNatPow` `SeparationQuotient` `instPow`	—	—
`mk_smul` 📖	mathematical	—	`SeparationQuotient` `instSMul`	—	—
`mk_sub` 📖	mathematical	—	`SeparationQuotient` `instSub`	—	—
`mk_vadd` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `SeparationQuotient` `instVAdd`	—	—
`mk_zpow` 📖	mathematical	—	`DivInvMonoid.toZPow` `Group.toDivInvMonoid` `SeparationQuotient` `instZPow`	—	—
`mk_zsmul` 📖	mathematical	—	`SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `SeparationQuotient` `instZSMul`	—	—

---

← Back to Index