Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `topologicalSpace`, `topologicalClosure`, `linearMapOfMemClosureRangeCoe`, `linearMapOfTendsto`	4
Theorems `of_continuousConstSMul`, `of_nhds_zero`, `submodule_topologicalClosure_eq`, `continuous_on_pi`, `isClosed_range_coe`, `punctured_nhds_neBot`, `closure_coe_iSup_map_single`, `closure_subset_topologicalClosure_span`, `continuousSMul_quotient`, `dense_iff_topologicalClosure_eq_top`, `eq_top_of_nonempty_interior'`, `isClosed_or_dense_of_isCoatom`, `isClosed_topologicalClosure`, `isOpenMap_mkQ`, `isOpenQuotientMap_mkQ`, `le_topologicalClosure`, `mapsTo_smul_closure`, `smul_closure_subset`, `t3_quotient_of_isClosed`, `topologicalAddGroup`, `topologicalAddGroup_quotient`, `completeSpace`, `topologicalClosure_coe`, `topologicalClosure_iSup_map_single`, `topologicalClosure_minimal`, `topologicalClosure_mono`, `span`, `continuousSMul_induced`, `continuousSMul_inducedₛₗ`, `instCompleteSpaceSubtypeMemSubmoduleOfIsClosedCoe`, `linearMapOfMemClosureRangeCoe_apply`, `linearMapOfTendsto_apply`	32
Total	36

ContinuousNeg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_continuousConstSMul` 📖	mathematical	—	`ContinuousNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`neg_smul` `one_smul` `ContinuousConstSMul.continuous_const_smul`

ContinuousSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_nhds_zero` 📖	mathematical	`Filter.Tendsto` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`ContinuousSMul`	—	`continuous_of_continuousAt_zero₂` `IsTopologicalRing.to_topologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `smul_zero` `nhds_prod_eq` `zero_smul`

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`submodule_topologicalClosure_eq` 📖	mathematical	—	`Submodule.topologicalClosure`	—	`SetLike.ext'` `closure_eq`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_on_pi` 📖	mathematical	—	`Continuous` `Pi.topologicalSpace` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `instFunLike`	—	`nonempty_fintype` `pi_apply_eq_sum_univ` `continuous_finset_sum` `Continuous.smul` `continuous_apply` `continuous_const`
`isClosed_range_coe` 📖	mathematical	—	`IsClosed` `Pi.topologicalSpace` `Set.range` `LinearMap` `DFunLike.coe` `instFunLike`	—	`isClosed_of_closure_subset`

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`punctured_nhds_neBot` 📖	mathematical	—	`Filter.NeBot` `nhdsWithin` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`exists_ne` `Filter.Tendsto.inf` `zero_smul` `add_zero` `Filter.Tendsto.add` `tendsto_const_nhds` `Filter.Tendsto.smul_const` `Filter.tendsto_id` `Filter.tendsto_principal_principal` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsDomain.toIsCancelMulZero` `Filter.Tendsto.neBot`

QuotientModule.Quotient

Definitions

Name	Category	Theorems
`topologicalSpace` 📖	CompOp	6 math math: `Submodule.t3_quotient_of_isClosed`, `Submodule.isOpenQuotientMap_mkQ`, `IsModuleTopology.instQuot`, `Submodule.isOpenMap_mkQ`, `Submodule.topologicalAddGroup_quotient`, `Submodule.continuousSMul_quotient`

Submodule

Definitions

Name	Category	Theorems
`topologicalClosure` 📖	CompOp	32 math math: `topologicalClosure_minimal`, `span_fourier_closure_eq_top`, `dense_iff_topologicalClosure_eq_top`, `closure_subset_topologicalClosure_span`, `IsClosed.submodule_topologicalClosure_eq`, `compactOperator_topologicalClosure`, `isClosed_topologicalClosure`, `topologicalClosure_map`, `topologicalClosure_eq_self`, `le_topologicalClosure`, `HilbertBasis.dense_span`, `orthogonal_orthogonal_eq_closure`, `orthogonal_closure`, `topologicalClosure_mono`, `topologicalClosure_coe`, `span_fourierLp_closure_eq_top`, `topologicalClosure_eq_top_iff`, `OrthogonalFamily.range_linearIsometry`, `LinearPMap.closure_def`, `ContinuousLinearMap.closed_range_of_antilipschitz`, `UnitAddTorus.span_mFourier_closure_eq_top`, `LinearPMap.closure_inverse_graph`, `topologicalClosure_iSup_map_single`, `UnitAddTorus.span_mFourierLp_closure_eq_top`, `ContinuousLinearMap.bijective_iff_dense_range_and_antilipschitz`, `LinearPMap.IsClosable.graph_closure_eq_closure_graph`, `topologicalClosure.completeSpace`, `starProjection_tendsto_closure_iSup`, `mem_closure_iff`, `ContinuousLinearMap.orthogonal_ker`, `LinearPMap.IsClosable.existsUnique`, `HilbertBasis.finite_spans_dense`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_coe_iSup_map_single` 📖	mathematical	—	`closure` `Pi.topologicalSpace` `SetLike.coe` `Submodule` `Pi.addCommMonoid` `Pi.module` `setLike` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `map` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.single` `Set.pi` `Set.univ`	—	`RingHomSurjective.ids` `closure_pi_set` `HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `closure_mono` `SetLike.coe_mono` `instIsConcreteLE` `iSup_map_single_le` `closure_minimal` `isOpen_pi_iff` `Finset.sum_apply` `Finset.sum_pi_single` `sum_mem` `addSubmonoidClass` `mem_iSup_of_mem` `mem_map_of_mem` `Set.mem_univ` `isClosed_closure`
`closure_subset_topologicalClosure_span` 📖	mathematical	—	`Set` `Set.instHasSubset` `closure` `SetLike.coe` `Submodule` `setLike` `topologicalClosure` `span`	—	`topologicalClosure_coe` `closure_mono` `subset_span`
`continuousSMul_quotient` 📖	mathematical	—	`ContinuousSMul` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `hasQuotient` `Quotient.instSMul` `QuotientModule.Quotient.topologicalSpace`	—	`IsOpenQuotientMap.continuous_comp_iff` `IsOpenQuotientMap.prodMap` `IsOpenQuotientMap.id` `isOpenQuotientMap_mkQ` `IsTopologicalAddGroup.toContinuousAdd` `Continuous.comp` `ContinuousSMul.continuous_smul`
`dense_iff_topologicalClosure_eq_top` 📖	mathematical	—	`Dense` `SetLike.coe` `Submodule` `setLike` `topologicalClosure` `Top.top` `instTop`	—	`SetLike.coe_set_eq` `dense_iff_closure_eq`
`eq_top_of_nonempty_interior'` 📖	mathematical	`Set.Nonempty` `interior` `SetLike.coe` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `setLike`	`Top.top` `instTop`	—	`eq_top_iff'` `Filter.Tendsto.add` `tendsto_const_nhds` `Filter.Tendsto.smul` `tendsto_nhdsWithin_of_tendsto_nhds` `Filter.tendsto_id` `Filter.nonempty_of_mem` `Filter.inter_mem` `Filter.mem_map` `add_zero` `zero_smul` `mem_interior_iff_mem_nhds` `self_mem_nhdsWithin` `mem_of_mem_nhds` `smul_mem_iff'` `Units.instIsScalarTower` `IsScalarTower.left` `Units.smul_def` `add_mem_iff_right`
`isClosed_or_dense_of_isCoatom` 📖	mathematical	`IsCoatom` `Submodule` `PartialOrder.toPreorder` `instPartialOrder` `instOrderTop`	`IsClosed` `SetLike.coe` `setLike` `Dense`	—	`isClosed_closure` `dense_iff_topologicalClosure_eq_top` `IsCoatom.le_iff` `le_topologicalClosure`
`isClosed_topologicalClosure` 📖	mathematical	—	`IsClosed` `SetLike.coe` `Submodule` `setLike` `topologicalClosure`	—	`isClosed_closure`
`isOpenMap_mkQ` 📖	mathematical	—	`IsOpenMap` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `hasQuotient` `QuotientModule.Quotient.topologicalSpace` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Quotient.addCommGroup` `Quotient.module` `LinearMap.instFunLike` `mkQ`	—	`QuotientAddGroup.isOpenMap_coe`
`isOpenQuotientMap_mkQ` 📖	mathematical	—	`IsOpenQuotientMap` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `hasQuotient` `QuotientModule.Quotient.topologicalSpace` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Quotient.addCommGroup` `Quotient.module` `LinearMap.instFunLike` `mkQ`	—	—
`le_topologicalClosure` 📖	mathematical	—	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `topologicalClosure`	—	`subset_closure`
`mapsTo_smul_closure` 📖	mathematical	—	`Set.MapsTo` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `closure` `SetLike.coe` `Submodule` `setLike`	—	`smul_mem` `Set.MapsTo.closure` `ContinuousConstSMul.continuous_const_smul`
`smul_closure_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `closure` `SetLike.coe` `Submodule` `setLike`	—	`Set.MapsTo.image_subset` `mapsTo_smul_closure`
`t3_quotient_of_isClosed` 📖	mathematical	—	`T3Space` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `hasQuotient` `QuotientModule.Quotient.topologicalSpace`	—	`QuotientAddGroup.instT3Space` `AddSubgroup.normal_of_comm`
`topologicalAddGroup` 📖	mathematical	—	`IsTopologicalAddGroup` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `instTopologicalSpaceSubtype` `AddCommGroup.toAddGroup` `addCommGroup`	—	`AddSubgroup.instIsTopologicalAddGroupSubtypeMem`
`topologicalAddGroup_quotient` 📖	mathematical	—	`IsTopologicalAddGroup` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `hasQuotient` `QuotientModule.Quotient.topologicalSpace` `AddCommGroup.toAddGroup` `Quotient.addCommGroup`	—	`AddSubgroup.normal_of_comm` `QuotientAddGroup.instIsTopologicalAddGroup`
`topologicalClosure_coe` 📖	mathematical	—	`SetLike.coe` `Submodule` `setLike` `topologicalClosure` `closure`	—	—
`topologicalClosure_iSup_map_single` 📖	mathematical	`ContinuousAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ContinuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`topologicalClosure` `Pi.topologicalSpace` `Pi.addCommMonoid` `Pi.module` `instContinuousConstSMulForall` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Pi.continuousAdd` `AddSemigroup.toAdd` `iSup` `Submodule` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `map` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.single` `pi` `Set.univ`	—	`SetLike.coe_injective` `instContinuousConstSMulForall` `Pi.continuousAdd` `RingHomSurjective.ids` `closure_coe_iSup_map_single`
`topologicalClosure_minimal` 📖	mathematical	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`topologicalClosure`	—	`closure_minimal`
`topologicalClosure_mono` 📖	mathematical	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`topologicalClosure`	—	`closure_mono`

Submodule.topologicalClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeSpace` 📖	mathematical	—	`CompleteSpace` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.topologicalClosure` `UniformSpace.toTopologicalSpace` `instUniformSpaceSubtype`	—	`IsClosed.completeSpace_coe` `isClosed_closure`

TopologicalSpace.IsSeparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`span` 📖	mathematical	`TopologicalSpace.IsSeparable`	`SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span`	—	`Submodule.span_eq_iUnion_nat` `iUnion` `instCountableNat` `image` `TopologicalSpace.isSeparable_pi` `instCountableFin` `prod` `of_separableSpace` `Set.univ_prod` `continuous_finset_sum` `Continuous.smul` `Continuous.comp` `continuous_fst` `continuous_apply` `continuous_snd`

(root)

Definitions

Name	Category	Theorems
`linearMapOfMemClosureRangeCoe` 📖	CompOp	1 math math: `linearMapOfMemClosureRangeCoe_apply`
`linearMapOfTendsto` 📖	CompOp	1 math math: `linearMapOfTendsto_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousSMul_induced` 📖	mathematical	—	`ContinuousSMul` `TopologicalSpace.induced` `DFunLike.coe`	—	`continuousSMul_inducedₛₗ` `continuous_id`
`continuousSMul_inducedₛₗ` 📖	mathematical	`Continuous`	`ContinuousSMul` `TopologicalSpace.induced` `DFunLike.coe`	—	`Topology.IsInducing.continuousSMul` `MulActionSemiHomClass.map_smulₛₗ`
`instCompleteSpaceSubtypeMemSubmoduleOfIsClosedCoe` 📖	mathematical	—	`CompleteSpace` `Submodule` `SetLike.instMembership` `Submodule.setLike` `instUniformSpaceSubtype`	—	`IsComplete.completeSpace_coe` `IsClosed.isComplete`
`linearMapOfMemClosureRangeCoe_apply` 📖	mathematical	`Set` `Set.instMembership` `closure` `Pi.topologicalSpace` `Set.range` `LinearMap` `DFunLike.coe` `LinearMap.instFunLike`	`linearMapOfMemClosureRangeCoe` `ZeroHom.toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.toZeroHom` `addMonoidHomOfMemClosureRangeCoe`	—	—
`linearMapOfTendsto_apply` 📖	mathematical	`Filter.Tendsto` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `nhds` `Pi.topologicalSpace`	`linearMapOfTendsto`	—	—

---

← Back to Index