Quotient

📁 Source: Mathlib/Topology/Algebra/Group/Quotient.lean

Statistics

Metric	Count
Definitions instTopologicalSpace, instTopologicalSpace	2
Theorems continuous_mk, dense_image_mk, dense_preimage_mk, discreteTopology, discreteTopology_iff, instCompactSpaceQuotientAddSubgroup, instContinuousConstVAdd, instContinuousVAdd, instFirstCountableTopology, instIsTopologicalAddGroup, instLocallyCompactSpace, instSecondCountableTopology, instT1Space, instT3Space, isClosedMap_coe, isOpenMap_coe, isOpenQuotientMap_mk, isQuotientMap_mk, nhds_eq, t1Space_iff, continuous_mk, dense_image_mk, dense_preimage_mk, discreteTopology, discreteTopology_iff, instCompactSpaceQuotientSubgroup, instContinuousConstSMul, instContinuousSMul, instFirstCountableTopology, instIsTopologicalGroup, instLocallyCompactSpace, instSecondCountableTopology, instT1Space, instT3Space, isClosedMap_coe, isOpenMap_coe, isOpenQuotientMap_mk, isQuotientMap_mk, nhds_eq, t1Space_iff	40
Total	42

QuotientAddGroup

Definitions

Name	Category	Theorems
instTopologicalSpace 📖	CompOp	130 math math: instT3Space, AddCircle.isAddQuotientCoveringMap_zsmul_of_ne_zero, Real.tsum_eq_tsum_fourier, AddCircle.liftIoc_zero_continuous, completeSpace_right', AddCircle.homeomorphCircle'_apply_mk, span_fourier_closure_eq_top, Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay_of_summable, hasSum_one_div_nat_pow_mul_fourier, AddCircle.toCircle_add, AddCircle.liftIco_continuous, UnitAddTorus.mFourierSubalgebra_coe, AddCircle.isAddQuotientCoveringMap_nsmul_of_ne_zero, UnitAddTorus.mFourierSubalgebra_closure_eq_top, AddCircle.homeomorphAddCircle_apply_mk, AddCircle.homeomorphCircle'_symm_apply, isOpenQuotientMap_mk, AddCircle.isAddQuotientCoveringMap_nsmul, completeSpace_left, instSecondCountableTopology, Polynomial.toAddCircle_X_pow_eq_fourier, fourier_norm, AddCircle.isAddQuotientCoveringMap_coe, AddCircle.isLocalHomeomorph_coe, instContinuousVAdd, UnitAddTorus.mFourierCoeff_toLp, isOpenMap_coe, AddCircle.instIsAddHaarMeasureRealVolume, AddCircle.ergodic_nsmul_add, AddCircle.dense_addSubgroup_iff_ne_zmultiples, completeSpace_right, fourier_one, AddCircle.denseRange_zsmul_iff, Polynomial.toAddCircle.integrable, fourier_zero, fourier_neg', AddCircle.ergodic_add_left, UnitAddTorus.mFourier_add, AddSubgroup.isAddQuotientCoveringMap_of_comm, AddCircle.ergodic_add_right, UnitAddTorus.mFourier_zero, discreteTopology_iff, UnitAddTorus.coeFn_mFourierLp, Real.tsum_eq_tsum_fourier_of_rpow_decay_of_summable, UnitAddTorus.mFourier_neg, t1Space_iff, instIsTopologicalAddGroup, AddCircle.continuous_equivIoc_symm, instT2Space, fourier_coe_apply, periodizedBernoulli.continuous, fourierSubalgebra_separatesPoints, AddSubgroup.discreteTopology, has_antideriv_at_fourier_neg, UnitAddTorus.mFourier_norm, instCompactSpaceQuotientAddSubgroup, hasDerivAt_fourier_neg, fourier_eval_zero, fourierCoeff_toLp, nhds_zero_hasBasis, AddCircle.continuous_toCircle, AddSubgroup.isAddQuotientCoveringMap, hasDerivAt_fourier, fourier_apply, AddCircle.openPartialHomeomorphCoe_source, dense_image_mk, AddCircle.denseRange_zsmul_coe_iff, fourierSubalgebra_coe, Polynomial.toAddCircle_monomial_eq_smul_fourier, AddSubgroup.instDiscreteTopologyQuotientOfContinuousAdd, instLocallyCompactSpace, AddCircle.compactSpace, UnitAddTorus.mFourierSubalgebra_separatesPoints, fourierCoeff_eq_intervalIntegral, instFirstCountableTopology, AddCircle.continuous_mk', Polynomial.fourierCoeff_toAddCircle_natCast, dense_preimage_mk, fourierCoeffOn_of_hasDerivAt_Ioo, instContinuousConstVAdd, isQuotientMap_mk, AddCircle.liftIoc_continuous, fourier_neg, AddCircle.continuous_equivIco_symm, Real.tsum_eq_tsum_fourier_of_rpow_decay, AddCircle.continuousAt_equivIoc, isClosedMap_coe, AddCircle.continuousAt_equivIco, AddCircle.openPartialHomeomorphCoe_symm_apply, fourierSubalgebra_closure_eq_top, continuous_mk, AddCircle.isAddQuotientCoveringMap_zsmul, nhds_eq, AddCircle.openPartialHomeomorphCoe_apply, UnitAddTorus.span_mFourier_closure_eq_top, fourierCoeffOn_eq_integral, UnitAddTorus.mFourier_single, AddCircle.liftIco_zero_continuous, discreteTopology, hasSum_one_div_pow_mul_fourier_mul_bernoulliFun, fourier_add', MeasureTheory.Integrable.fourier_smul, Polynomial.toAddCircle_X_eq_fourier_one, fourier_add_half_inv_index, fourierCoeffOn_of_hasDerivAt, borelSpace, AddCircle.pathConnectedSpace, Real.tsum_eq_tsum_fourierIntegral, SchwartzMap.tsum_eq_tsum_fourierIntegral, fourier_add, MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addHaarMeasure_quotient, instT1Space, Polynomial.toAddCircle_C_eq_smul_fourier_zero, AddCircle.isCoveringMap_coe, AddCircle.homeomorphCircle'_apply, instIsAddHaarMeasureUnitAddCircleVolume, AddCircle.homeomorphCircle_apply, Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay, Polynomial.fourierCoeff_toAddCircle, fourierCoeffOn_of_hasDeriv_right, coeFn_fourierLp, AddCircle.openPartialHomeomorphCoe_target, AddCosetSpace.borelSpace, completeSpace_left', AddCircle.ergodic_zsmul_add, AddCircle.homeomorphAddCircle_symm_apply_mk, SchwartzMap.tsum_eq_tsum_fourier, Polynomial.fourierCoeff_toAddCircle_eq_zero_of_lt_zero, IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_vaddAddHaarMeasure, fourierCoeff_fourier

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_mk 📖	mathematical	—	Continuous HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup instTopologicalSpace	—	—
dense_image_mk 📖	mathematical	—	Dense HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup instTopologicalSpace Set.image Set Set.add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SetLike.coe AddSubgroup.instSetLike	—	preimage_image_mk_eq_add
dense_preimage_mk 📖	mathematical	—	Dense Set.preimage HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup instTopologicalSpace	—	IsOpenQuotientMap.dense_preimage_iff
discreteTopology 📖	mathematical	IsOpen SetLike.coe AddSubgroup AddSubgroup.instSetLike	DiscreteTopology HasQuotient.Quotient instHasQuotientAddSubgroup instTopologicalSpace	—	discreteTopology_iff
discreteTopology_iff 📖	mathematical	—	DiscreteTopology HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup instTopologicalSpace IsOpen SetLike.coe AddSubgroup.instSetLike	—	preimage_mk_zero AddAction.IsPretransitive.discreteTopology_iff AddAction.left_quotientAction instContinuousConstVAdd AddAction.isPretransitive_quotient isOpen_coinduced
instCompactSpaceQuotientAddSubgroup 📖	mathematical	—	CompactSpace HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup instTopologicalSpace	—	Quotient.compactSpace
instContinuousConstVAdd 📖	mathematical	—	ContinuousConstVAdd HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup instTopologicalSpace AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddAction.quotient AddMonoid.toAddAction AddAction.left_quotientAction	—	AddAction.left_quotientAction ContinuousVAdd.continuousConstVAdd instContinuousVAdd
instContinuousVAdd 📖	mathematical	—	ContinuousVAdd HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddAction.quotient AddMonoid.toAddAction AddAction.left_quotientAction instTopologicalSpace	—	AddAction.left_quotientAction IsOpenQuotientMap.continuous_comp_iff IsOpenQuotientMap.prodMap IsOpenQuotientMap.id Continuous.comp continuous_add
instFirstCountableTopology 📖	mathematical	—	FirstCountableTopology HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup instTopologicalSpace	—	Function.Surjective.forall mk_surjective Filter.map.isCountablyGenerated FirstCountableTopology.nhds_generated_countable nhds_eq
instIsTopologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup instTopologicalSpace Quotient.addGroup	—	IsOpenQuotientMap.continuous_comp_iff IsOpenQuotientMap.prodMap IsTopologicalAddGroup.toContinuousAdd Continuous.comp continuous_add Continuous.quotient_map' ContinuousNeg.continuous_neg IsTopologicalAddGroup.toContinuousNeg AddCon.neg
instLocallyCompactSpace 📖	mathematical	—	LocallyCompactSpace HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup instTopologicalSpace	—	IsOpenQuotientMap.locallyCompactSpace
instSecondCountableTopology 📖	mathematical	—	SecondCountableTopology HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup instTopologicalSpace	—	ContinuousConstVAdd.secondCountableTopology VAddCommClass.continuousConstVAdd AddSubgroup.vaddCommClass_left AddSemigroup.opposite_vaddCommClass
instT1Space 📖	mathematical	—	T1Space HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup instTopologicalSpace	—	t1Space_iff
instT3Space 📖	mathematical	—	T3Space HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup instTopologicalSpace	—	instT3Space T1Space.t0Space instT1Space IsTopologicalAddGroup.toContinuousAdd IsTopologicalAddGroup.regularSpace instIsTopologicalAddGroup
isClosedMap_coe 📖	mathematical	IsCompact SetLike.coe AddSubgroup AddSubgroup.instSetLike	IsClosedMap HasQuotient.Quotient instHasQuotientAddSubgroup instTopologicalSpace	—	Topology.IsQuotientMap.isClosed_preimage preimage_image_mk_eq_add IsClosed.add_right_of_isCompact
isOpenMap_coe 📖	mathematical	—	IsOpenMap HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup instTopologicalSpace	—	isOpenMap_quotient_mk'_add VAddCommClass.continuousConstVAdd AddSubgroup.vaddCommClass_left AddSemigroup.opposite_vaddCommClass
isOpenQuotientMap_mk 📖	mathematical	—	IsOpenQuotientMap HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup instTopologicalSpace	—	AddAction.isOpenQuotientMap_quotientMk VAddCommClass.continuousConstVAdd AddSubgroup.vaddCommClass_left AddSemigroup.opposite_vaddCommClass
isQuotientMap_mk 📖	mathematical	—	Topology.IsQuotientMap HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup instTopologicalSpace	—	—
nhds_eq 📖	mathematical	—	nhds HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup instTopologicalSpace Filter.map	—	IsOpenQuotientMap.map_nhds_eq
t1Space_iff 📖	mathematical	—	T1Space HasQuotient.Quotient AddSubgroup instHasQuotientAddSubgroup instTopologicalSpace IsClosed SetLike.coe AddSubgroup.instSetLike	—	preimage_mk_zero AddAction.IsPretransitive.t1Space_iff AddAction.left_quotientAction instContinuousConstVAdd AddAction.isPretransitive_quotient isClosed_coinduced

QuotientGroup

Definitions

Name	Category	Theorems
instTopologicalSpace 📖	CompOp	34 math math: isQuotientMap_mk, discreteTopology, instSecondCountableTopology, borelSpace, nhds_eq, completeSpace_left, Subgroup.instDiscreteTopologyQuotientOfContinuousMul, isClosedMap_coe, completeSpace_right, MeasureTheory.QuotientMeasureEqMeasurePreimage.haarMeasure_quotient, Subgroup.discreteTopology, completeSpace_right', nhds_one_hasBasis, instT2Space, dense_preimage_mk, discreteTopology_iff, instT3Space, continuous_mk, instContinuousSMul, completeSpace_left', isOpenMap_coe, IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_smulHaarMeasure, Subgroup.isQuotientCoveringMap_of_comm, CosetSpace.borelSpace, instContinuousConstSMul, instT1Space, isOpenQuotientMap_mk, instFirstCountableTopology, instLocallyCompactSpace, instIsTopologicalGroup, dense_image_mk, instCompactSpaceQuotientSubgroup, Subgroup.isQuotientCoveringMap, t1Space_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_mk 📖	mathematical	—	Continuous HasQuotient.Quotient Subgroup instHasQuotientSubgroup instTopologicalSpace	—	—
dense_image_mk 📖	mathematical	—	Dense HasQuotient.Quotient Subgroup instHasQuotientSubgroup instTopologicalSpace Set.image Set Set.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SetLike.coe Subgroup.instSetLike	—	preimage_image_mk_eq_mul
dense_preimage_mk 📖	mathematical	—	Dense Set.preimage HasQuotient.Quotient Subgroup instHasQuotientSubgroup instTopologicalSpace	—	IsOpenQuotientMap.dense_preimage_iff
discreteTopology 📖	mathematical	IsOpen SetLike.coe Subgroup Subgroup.instSetLike	DiscreteTopology HasQuotient.Quotient instHasQuotientSubgroup instTopologicalSpace	—	discreteTopology_iff
discreteTopology_iff 📖	mathematical	—	DiscreteTopology HasQuotient.Quotient Subgroup instHasQuotientSubgroup instTopologicalSpace IsOpen SetLike.coe Subgroup.instSetLike	—	preimage_mk_one MulAction.IsPretransitive.discreteTopology_iff MulAction.left_quotientAction instContinuousConstSMul MulAction.isPretransitive_quotient isOpen_coinduced
instCompactSpaceQuotientSubgroup 📖	mathematical	—	CompactSpace HasQuotient.Quotient Subgroup instHasQuotientSubgroup instTopologicalSpace	—	Quotient.compactSpace
instContinuousConstSMul 📖	mathematical	—	ContinuousConstSMul HasQuotient.Quotient Subgroup instHasQuotientSubgroup instTopologicalSpace SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction MulAction.quotient Monoid.toMulAction MulAction.left_quotientAction	—	MulAction.left_quotientAction ContinuousSMul.continuousConstSMul instContinuousSMul
instContinuousSMul 📖	mathematical	—	ContinuousSMul HasQuotient.Quotient Subgroup instHasQuotientSubgroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction MulAction.quotient Monoid.toMulAction MulAction.left_quotientAction instTopologicalSpace	—	MulAction.left_quotientAction IsOpenQuotientMap.continuous_comp_iff IsOpenQuotientMap.prodMap IsOpenQuotientMap.id Continuous.comp continuous_mul
instFirstCountableTopology 📖	mathematical	—	FirstCountableTopology HasQuotient.Quotient Subgroup instHasQuotientSubgroup instTopologicalSpace	—	Function.Surjective.forall mk_surjective Filter.map.isCountablyGenerated FirstCountableTopology.nhds_generated_countable nhds_eq
instIsTopologicalGroup 📖	mathematical	—	IsTopologicalGroup HasQuotient.Quotient Subgroup instHasQuotientSubgroup instTopologicalSpace Quotient.group	—	IsOpenQuotientMap.continuous_comp_iff IsOpenQuotientMap.prodMap IsTopologicalGroup.toContinuousMul Continuous.comp continuous_mul Continuous.quotient_map' ContinuousInv.continuous_inv IsTopologicalGroup.toContinuousInv Con.inv
instLocallyCompactSpace 📖	mathematical	—	LocallyCompactSpace HasQuotient.Quotient Subgroup instHasQuotientSubgroup instTopologicalSpace	—	IsOpenQuotientMap.locallyCompactSpace
instSecondCountableTopology 📖	mathematical	—	SecondCountableTopology HasQuotient.Quotient Subgroup instHasQuotientSubgroup instTopologicalSpace	—	ContinuousConstSMul.secondCountableTopology SMulCommClass.continuousConstSMul Subgroup.smulCommClass_left Semigroup.opposite_smulCommClass
instT1Space 📖	mathematical	—	T1Space HasQuotient.Quotient Subgroup instHasQuotientSubgroup instTopologicalSpace	—	t1Space_iff
instT3Space 📖	mathematical	—	T3Space HasQuotient.Quotient Subgroup instHasQuotientSubgroup instTopologicalSpace	—	instT3Space T1Space.t0Space instT1Space IsTopologicalGroup.toContinuousMul IsTopologicalGroup.regularSpace instIsTopologicalGroup
isClosedMap_coe 📖	mathematical	IsCompact SetLike.coe Subgroup Subgroup.instSetLike	IsClosedMap HasQuotient.Quotient instHasQuotientSubgroup instTopologicalSpace	—	Topology.IsQuotientMap.isClosed_preimage preimage_image_mk_eq_mul IsClosed.mul_right_of_isCompact
isOpenMap_coe 📖	mathematical	—	IsOpenMap HasQuotient.Quotient Subgroup instHasQuotientSubgroup instTopologicalSpace	—	isOpenMap_quotient_mk'_mul SMulCommClass.continuousConstSMul Subgroup.smulCommClass_left Semigroup.opposite_smulCommClass
isOpenQuotientMap_mk 📖	mathematical	—	IsOpenQuotientMap HasQuotient.Quotient Subgroup instHasQuotientSubgroup instTopologicalSpace	—	MulAction.isOpenQuotientMap_quotientMk SMulCommClass.continuousConstSMul Subgroup.smulCommClass_left Semigroup.opposite_smulCommClass
isQuotientMap_mk 📖	mathematical	—	Topology.IsQuotientMap HasQuotient.Quotient Subgroup instHasQuotientSubgroup instTopologicalSpace	—	—
nhds_eq 📖	mathematical	—	nhds HasQuotient.Quotient Subgroup instHasQuotientSubgroup instTopologicalSpace Filter.map	—	IsOpenQuotientMap.map_nhds_eq
t1Space_iff 📖	mathematical	—	T1Space HasQuotient.Quotient Subgroup instHasQuotientSubgroup instTopologicalSpace IsClosed SetLike.coe Subgroup.instSetLike	—	preimage_mk_one MulAction.IsPretransitive.t1Space_iff MulAction.left_quotientAction instContinuousConstSMul MulAction.isPretransitive_quotient isClosed_coinduced

---

← Back to Index