ModuleTopology

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

Statistics

Metric	Count
Definitions `IsModuleTopology`, `moduleTopology`	2
Theorems `continuousNeg`, `continuous_bilinear_of_finite_left`, `continuous_bilinear_of_finite_right`, `continuous_bilinear_of_pi_fintype`, `continuous_mul_of_finite`, `continuous_neg`, `continuous_of_distribMulActionHom`, `continuous_of_distribMulActionHomₑ`, `continuous_of_linearMap`, `continuous_of_linearMapₛₗ`, `continuous_of_ringHom`, `eq_moduleTopology'`, `instPi`, `instProd`, `instQuot`, `instSubsingleton`, `isOpenMap_of_surjective`, `isOpenMap_of_surjectiveₛₗ`, `isOpenQuotientMap_of_surjective`, `isOpenQuotientMap_of_surjectiveₛₗ`, `isQuotientMap_of_surjective`, `isQuotientMap_of_surjectiveₛₗ`, `isTopologicalRing`, `iso`, `isoₛₗ`, `of_continuous_id`, `toContinuousAdd`, `toContinuousSMul`, `topologicalAddGroup`, `toIsModuleTopology`, `toOppositeIsModuleTopology`, `continuousAdd`, `continuousSMul`, `eq_coinduced_of_surjective`, `eq_coinduced_of_surjectiveₛₗ`, `eq_moduleTopology`, `instIsModuleTopology`, `moduleTopology_le`	38
Total	40

IsModuleTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousNeg` 📖	mathematical	—	`ContinuousNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`continuous_neg`
`continuous_bilinear_of_finite_left` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing`	—	`smulCommClass_self` `Module.Finite.exists_fin'` `RingHomCompTriple.ids` `Function.Surjective.prodMap` `Topology.IsQuotientMap.continuous_iff` `isQuotientMap_of_surjective` `instProd` `instPi` `Finite.of_fintype` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `continuous_bilinear_of_pi_fintype`
`continuous_bilinear_of_finite_right` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing`	—	`smulCommClass_self` `SMulCommClass.symm` `Continuous.comp'` `continuous_bilinear_of_finite_left` `Continuous.prodMk` `Continuous.snd` `continuous_id'` `Continuous.fst`
`continuous_bilinear_of_pi_fintype` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd` `Pi.topologicalSpace` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.addCommMonoid` `Pi.Function.module` `Semiring.toModule` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`smulCommClass_self` `nonempty_fintype` `Finset.univ_sum_single` `Finset.sum_congr` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `LinearMap.coe_sum` `Finset.sum_apply` `Finsupp.smul_single_one` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `continuous_finset_sum` `toContinuousAdd` `Continuous.smul` `toContinuousSMul` `Continuous.comp'` `continuous_apply` `Continuous.fst` `continuous_id'` `continuous_of_linearMap` `Continuous.snd`
`continuous_mul_of_finite` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`continuous_bilinear_of_finite_left` `Algebra.to_smulCommClass` `IsScalarTower.right`
`continuous_neg` 📖	mathematical	—	`Continuous` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`continuous_of_linearMap` `toContinuousAdd` `toContinuousSMul` `RingHomInvPair.ids`
`continuous_of_distribMulActionHom` 📖	mathematical	—	`Continuous` `DFunLike.coe` `DistribMulActionHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `DistribMulActionHom.instFunLike`	—	`continuous_of_distribMulActionHomₑ` `continuous_id`
`continuous_of_distribMulActionHomₑ` 📖	mathematical	`Continuous` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `MonoidHom.instFunLike`	`DistribMulActionHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `DistribMulActionHom.instFunLike`	—	`eq_moduleTopology` `continuous_iff_le_induced` `sInf_le` `continuousSMul_inducedₛₗ` `DistribMulActionSemiHomClass.toMulActionSemiHomClass` `DistribMulActionHom.instDistribMulActionSemiHomClassCoeMonoidHom` `continuousAdd_induced` `AddMonoidHomClass.toAddHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass`
`continuous_of_linearMap` 📖	mathematical	—	`Continuous` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	`continuous_of_distribMulActionHom`
`continuous_of_linearMapₛₗ` 📖	mathematical	`Continuous` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	`LinearMap` `LinearMap.instFunLike`	—	`continuous_of_distribMulActionHomₑ`
`continuous_of_ringHom` 📖	—	`Continuous` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `RingHom.comp` `algebraMap`	—	—	`AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Algebra.smul_def` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Continuous.mul` `IsTopologicalSemiring.toContinuousMul` `Continuous.comp` `continuous_fst` `continuous_snd` `continuous_of_linearMap` `IsTopologicalSemiring.toContinuousAdd`
`eq_moduleTopology'` 📖	mathematical	—	`moduleTopology`	—	—
`instPi` 📖	mathematical	`IsModuleTopology` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`Pi.instAdd` `Pi.instSMul` `Pi.topologicalSpace`	—	`Finite.induction_empty_option` `iso` `instSubsingleton` `Unique.instSubsingleton` `PEmpty.instIsEmpty` `RingHomInvPair.ids` `instProd`
`instProd` 📖	mathematical	—	`IsModuleTopology` `Prod.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Prod.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `instTopologicalSpaceProd`	—	`toContinuousAdd` `le_antisymm` `ModuleTopology.continuousAdd` `continuous_id_iff_le` `add_zero` `zero_add` `Continuous.fun_add` `Continuous.comp'` `continuous_of_linearMap` `toContinuousSMul` `Continuous.fst` `continuous_id'` `Continuous.snd` `sInf_le` `Prod.continuousSMul` `Prod.continuousAdd`
`instQuot` 📖	mathematical	—	`IsModuleTopology` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.instSMul` `QuotientModule.Quotient.topologicalSpace`	—	`toContinuousAdd` `Topology.IsQuotientMap.eq_coinduced` `IsOpenQuotientMap.isQuotientMap` `Submodule.isOpenQuotientMap_mkQ` `ModuleTopology.eq_coinduced_of_surjective` `Submodule.mkQ_surjective`
`instSubsingleton` 📖	mathematical	—	`IsModuleTopology`	—	`Unique.instSubsingleton`
`isOpenMap_of_surjective` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`IsOpenMap`	—	`isOpenMap_of_surjectiveₛₗ` `IsOpenQuotientMap.id`
`isOpenMap_of_surjectiveₛₗ` 📖	mathematical	`IsOpenQuotientMap` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike` `LinearMap` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`IsOpenMap`	—	`IsOpenQuotientMap.isOpenMap` `isOpenQuotientMap_of_surjectiveₛₗ` `moduleTopology_le`
`isOpenQuotientMap_of_surjective` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`IsOpenQuotientMap`	—	`isOpenQuotientMap_of_surjectiveₛₗ` `IsOpenQuotientMap.id`
`isOpenQuotientMap_of_surjectiveₛₗ` 📖	—	`IsOpenQuotientMap` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike` `LinearMap` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	—	—	`toContinuousAdd` `AddMonoidHom.isOpenQuotientMap_of_isQuotientMap` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `isQuotientMap_of_surjectiveₛₗ`
`isQuotientMap_of_surjective` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`Topology.IsQuotientMap`	—	`isQuotientMap_of_surjectiveₛₗ` `IsOpenQuotientMap.id`
`isQuotientMap_of_surjectiveₛₗ` 📖	mathematical	`IsOpenQuotientMap` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike` `LinearMap` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`Topology.IsQuotientMap`	—	`continuous_of_linearMapₛₗ` `toContinuousAdd` `toContinuousSMul` `IsOpenQuotientMap.continuous` `le_antisymm` `eq_moduleTopology` `AddMonoidHom.isOpenQuotientMap_of_isQuotientMap` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `sInf_le` `LinearMap.map_smulₛₗ` `IsOpenQuotientMap.prodMap` `IsOpenQuotientMap.continuous_comp_iff` `Continuous.comp` `map_add` `SemilinearMapClass.toAddHomClass` `continuous_iff_coinduced_le`
`isTopologicalRing` 📖	mathematical	—	`IsTopologicalRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`toContinuousAdd` `continuous_mul_of_finite` `continuous_neg`
`iso` 📖	mathematical	—	`IsModuleTopology` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`RingHomInvPair.ids` `isoₛₗ` `continuous_id`
`isoₛₗ` 📖	mathematical	`Continuous` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	`IsModuleTopology` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousSemilinearEquivClass.continuousSemilinearMapClass` `ContinuousLinearEquiv.continuousSemilinearEquivClass` `Topology.IsInducing.eq_induced` `Homeomorph.isInducing` `eq_moduleTopology` `induced_sInf` `Set.ext` `Set.mem_image` `continuousSMul_inducedₛₗ` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `continuousAdd_induced` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `induced_compose` `induced_id` `ContinuousLinearEquiv.self_comp_symm`
`of_continuous_id` 📖	mathematical	`Continuous` `moduleTopology`	`IsModuleTopology`	—	`le_antisymm` `continuous_id_iff_le` `moduleTopology_le`
`toContinuousAdd` 📖	mathematical	—	`ContinuousAdd`	—	`ModuleTopology.continuousAdd` `eq_moduleTopology`
`toContinuousSMul` 📖	mathematical	—	`ContinuousSMul`	—	`ModuleTopology.continuousSMul` `eq_moduleTopology`
`topologicalAddGroup` 📖	mathematical	—	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup`	—	`toContinuousAdd` `continuous_neg`

IsTopologicalSemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toIsModuleTopology` 📖	mathematical	—	`IsModuleTopology` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul`	—	`IsModuleTopology.of_continuous_id` `toContinuousAdd` `ContinuousMul.to_continuousSMul` `toContinuousMul` `mul_one` `Continuous.comp` `ContinuousSMul.continuous_smul` `ModuleTopology.continuousSMul` `Continuous.prodMk` `continuous_id` `continuous_const`
`toOppositeIsModuleTopology` 📖	mathematical	—	`IsModuleTopology` `MulOpposite` `MulOpposite.instTopologicalSpaceMulOpposite` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulOpposite.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `MulOpposite.instSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toOppositeModule`	—	`IsModuleTopology.iso` `toIsModuleTopology` `instIsTopologicalSemiringMulOpposite` `RingHomInvPair.ids`

ModuleTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAdd` 📖	mathematical	—	`ContinuousAdd` `moduleTopology`	—	`continuousAdd_sInf`
`continuousSMul` 📖	mathematical	—	`ContinuousSMul` `moduleTopology`	—	`continuousSMul_sInf`
`eq_coinduced_of_surjective` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`moduleTopology` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `TopologicalSpace.coinduced` `TopologicalSpace`	—	`eq_coinduced_of_surjectiveₛₗ` `IsOpenQuotientMap.id`
`eq_coinduced_of_surjectiveₛₗ` 📖	mathematical	`IsOpenQuotientMap` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike` `LinearMap` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`moduleTopology` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `TopologicalSpace.coinduced` `TopologicalSpace`	—	`Topology.IsQuotientMap.eq_coinduced` `IsModuleTopology.isQuotientMap_of_surjectiveₛₗ`

(root)

Definitions

Name	Category	Theorems
`IsModuleTopology` 📖	CompData	10 math math: `instIsModuleTopology`, `IsModuleTopology.of_continuous_id`, `isModuleTopologyOfFiniteDimensional`, `IsModuleTopology.instProd`, `IsTopologicalSemiring.toIsModuleTopology`, `IsModuleTopology.isoₛₗ`, `IsTopologicalSemiring.toOppositeIsModuleTopology`, `IsModuleTopology.iso`, `IsModuleTopology.instQuot`, `IsModuleTopology.instSubsingleton`
`moduleTopology` 📖	CompOp	8 math math: `instIsModuleTopology`, `ModuleTopology.continuousSMul`, `ModuleTopology.eq_coinduced_of_surjectiveₛₗ`, `ModuleTopology.eq_coinduced_of_surjective`, `eq_moduleTopology`, `IsModuleTopology.eq_moduleTopology'`, `moduleTopology_le`, `ModuleTopology.continuousAdd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_moduleTopology` 📖	mathematical	—	`moduleTopology`	—	`IsModuleTopology.eq_moduleTopology'`
`instIsModuleTopology` 📖	mathematical	—	`IsModuleTopology` `moduleTopology`	—	—
`moduleTopology_le` 📖	mathematical	—	`TopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder` `moduleTopology`	—	`sInf_le`

---

← Back to Index