Basic

📁 Source: Mathlib/Analysis/LocallyConvex/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `eq_univ_of_smulMemClass`, `eventually_nhdsNE_zero`, `submodule_eq_top`, `subset_range_iff_surjective`, `eventually_nhdsNE_zero`, `eventually_nhds_zero`, `exists_pos`, `of_norm`, `absorbs_self`, `add`, `closure`, `convexHull`, `inter`, `interior`, `mulActionHom_preimage`, `neg`, `neg_eq`, `neg_mem_iff`, `sInter`, `smul`, `smul_congr`, `smul_eq`, `smul_mem`, `smul_mem_iff`, `smul_mem_mono`, `smul_mono`, `sub`, `subset_smul`, `union`, `zero_insert_interior`, `absorbent_iff_eventually_nhdsNE_zero`, `absorbent_nhds_zero`, `absorbs_iff_eventually_nhdsNE_zero`, `absorbs_iff_eventually_nhds_zero`, `absorbs_iff_norm`, `balanced_empty`, `balanced_iInter`, `balanced_iInter₂`, `balanced_iUnion`, `balanced_iUnion₂`, `balanced_iff_closedBall_smul`, `balanced_iff_neg_mem`, `balanced_iff_smul_mem`, `balanced_neg`, `balanced_univ`, `balanced_zero`	46
Total	46

Absorbent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_univ_of_smulMemClass` 📖	mathematical	`Absorbent` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SetLike.coe`	`Set.univ`	—	`Set.eq_univ_iff_forall` `Filter.Eventually.exists` `NormedField.nhdsNE_neBot` `Filter.Eventually.and` `absorbent_iff_eventually_nhdsNE_zero` `eventually_mem_nhdsWithin` `inv_smul_smul₀` `SMulMemClass.smul_mem`
`eventually_nhdsNE_zero` 📖	mathematical	`Absorbent` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`Filter.Eventually` `Set` `Set.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Compl.compl` `Set.instCompl` `Set.instSingletonSet`	—	`absorbent_iff_eventually_nhdsNE_zero`
`submodule_eq_top` 📖	mathematical	`Absorbent` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SetLike.coe` `Submodule` `Submodule.setLike`	`Top.top` `Submodule.instTop`	—	`StrictMono.apply_eq_top_iff` `eq_univ_of_smulMemClass` `Submodule.smulMemClass`
`subset_range_iff_surjective` 📖	mathematical	`Absorbent` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`Set` `Set.instHasSubset` `SetLike.coe` `Submodule` `Submodule.setLike` `LinearMap.range` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	—	`LinearMap.range_eq_top` `submodule_eq_top` `mono`

Absorbs

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_nhdsNE_zero` 📖	mathematical	`Absorbs` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`Filter.Eventually` `Set.MapsTo` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`absorbs_iff_eventually_nhdsNE_zero`
`eventually_nhds_zero` 📖	mathematical	`Absorbs` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Set` `Set.instMembership` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Filter.Eventually` `Set.MapsTo` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`absorbs_iff_eventually_nhds_zero`
`exists_pos` 📖	mathematical	`Absorbs` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace`	`Real` `Real.instLT` `Real.instZero` `Set` `Set.instHasSubset` `Set.smulSet`	—	`Filter.HasBasis.eventually_iff` `Filter.HasBasis.cobounded_of_norm` `Filter.atTop_basis'` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `LT.lt.trans_le` `one_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`
`of_norm` 📖	mathematical	`Set` `Set.instHasSubset` `Set.smulSet`	`Absorbs` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace`	—	`absorbs_iff_norm`

Balanced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absorbs_self` 📖	mathematical	`Balanced` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`Absorbs` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace`	—	`Absorbs.of_norm` `subset_smul`
`add` 📖	mathematical	`Balanced` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`Set` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Eq.subset` `Set.instReflSubset` `smul_add` `Set.add_subset_add`
`closure` 📖	mathematical	`Balanced` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`closure`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `image_closure_subset_closure_image` `ContinuousConstSMul.continuous_const_smul` `ContinuousSMul.continuousConstSMul` `closure_mono`
`convexHull` 📖	mathematical	`Balanced` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`DFunLike.coe` `ClosureOperator` `Set` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull`	—	`smul_add` `SMulCommClass.smul_comm` `smulCommClass_self` `convex_convexHull` `balanced_iff_smul_mem` `convexHull_min` `subset_convexHull`
`inter` 📖	mathematical	`Balanced`	`Set` `Set.instInter`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.smul_set_inter_subset` `Set.inter_subset_inter`
`interior` 📖	—	`Balanced` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Set` `Set.instMembership` `interior` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—	`Set.insert_eq_self` `zero_insert_interior`
`mulActionHom_preimage` 📖	mathematical	`Balanced`	`Set.preimage` `DFunLike.coe` `MulActionHom` `instFunLikeMulActionHom`	—	`Set.mem_preimage` `map_smul` `instMulActionSemiHomClassMulActionHom` `Set.smul_mem_smul_set`
`neg` 📖	mathematical	`Balanced` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`Set` `Set.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`forall₂_imp` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Eq.subset` `Set.instReflSubset` `Set.smul_set_neg` `Set.neg_subset_neg`
`neg_eq` 📖	mathematical	`Balanced` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`Set` `Set.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Set.ext` `neg_mem_iff`
`neg_mem_iff` 📖	mathematical	`Balanced` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`Set` `Set.instMembership` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`smul_neg` `neg_smul` `one_smul` `neg_neg` `smul_mem` `norm_neg` `NormOneClass.norm_one`
`sInter` 📖	mathematical	`Balanced`	`Set.sInter`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.smul_set_sInter_subset`
`smul` 📖	mathematical	`Balanced`	`Set` `Set.smulSet`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Eq.subset` `Set.instReflSubset` `SMulCommClass.smul_comm` `Set.smulCommClass_set` `Set.smul_set_mono`
`smul_congr` 📖	mathematical	`Balanced` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Norm.norm` `NormedDivisionRing.toNorm`	`Set` `Set.smulSet`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `smul_mono` `NormMulClass.toNormSMulClass` `NormedDivisionRing.toNormMulClass` `IsScalarTower.left` `Eq.le` `Eq.ge`
`smul_eq` 📖	mathematical	`Balanced` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Norm.norm` `NormedDivisionRing.toNorm` `Real` `Real.instOne`	`Set` `Set.smulSet`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Eq.le` `subset_smul` `Eq.ge`
`smul_mem` 📖	—	`Balanced` `Real` `Real.instLE` `Norm.norm` `SeminormedRing.toNorm` `Real.instOne` `Set` `Set.instMembership`	—	—	`balanced_iff_smul_mem`
`smul_mem_iff` 📖	mathematical	`Balanced` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Norm.norm` `NormedField.toNorm`	`Set` `Set.instMembership`	—	`smul_mem_mono` `NormedSpace.toNormSMulClass` `IsScalarTower.left` `smulCommClass_self` `Eq.ge` `Eq.le`
`smul_mem_mono` 📖	—	`Balanced` `NormedRing.toSeminormedRing` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Set` `Set.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Real` `Real.instLE` `Norm.norm` `NormedRing.toNorm` `NormedDivisionRing.toNorm`	—	—	`eq_or_ne` `norm_zero` `zero_smul` `smul_mem` `norm_smul` `norm_inv` `div_eq_inv_mul` `div_le_one_of_le₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `Real.instZeroLEOneClass` `norm_nonneg` `SMulCommClass.smul_comm` `smul_assoc` `smul_inv_smul₀`
`smul_mono` 📖	mathematical	`Balanced` `NormedRing.toSeminormedRing` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Real` `Real.instLE` `Norm.norm` `NormedRing.toNorm` `NormedDivisionRing.toNorm`	`Set` `Set.instHasSubset` `Set.smulSet` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`eq_or_ne` `norm_le_zero_iff` `norm_zero` `Set.image_congr` `zero_smul` `smul_assoc` `Set.isScalarTower` `smul_inv_smul₀` `Set.smul_set_mono` `norm_smul` `norm_inv` `div_eq_inv_mul` `div_le_one_of_le₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `Real.instZeroLEOneClass` `norm_nonneg`
`sub` 📖	mathematical	`Balanced` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`Set` `Set.sub` `SubNegMonoid.toSub`	—	`sub_eq_add_neg` `add` `neg`
`subset_smul` 📖	mathematical	`Balanced` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Real` `Real.instLE` `Real.instOne` `Norm.norm` `NormedDivisionRing.toNorm`	`Set` `Set.instHasSubset` `Set.smulSet`	—	`one_smul` `smul_mono` `NormMulClass.toNormSMulClass` `NormedDivisionRing.toNormMulClass` `IsScalarTower.left` `NormOneClass.norm_one` `NormedDivisionRing.to_normOneClass`
`union` 📖	mathematical	`Balanced`	`Set` `Set.instUnion`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Eq.subset` `Set.instReflSubset` `Set.smul_set_union` `Set.union_subset_union`
`zero_insert_interior` 📖	mathematical	`Balanced` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`Set` `Set.instInsert` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `interior`	—	`eq_or_ne` `Set.zero_smul_set` `Set.subset_union_left` `Set.image_smul` `Set.image_insert_eq` `smul_zero` `Set.insert_subset_insert` `Set.MapsTo.image_subset` `IsOpenMap.mapsTo_interior` `isOpenMap_smul₀` `ContinuousSMul.continuousConstSMul` `smul_mem`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absorbent_iff_eventually_nhdsNE_zero` 📖	mathematical	—	`Absorbent` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Filter.Eventually` `Set` `Set.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Compl.compl` `Set.instCompl` `Set.instSingletonSet`	—	—
`absorbent_nhds_zero` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Absorbent` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`absorbent_iff_inv_smul` `Filter.Tendsto.smul` `Filter.tendsto_inv₀_cobounded` `tendsto_const_nhds` `zero_smul`
`absorbs_iff_eventually_nhdsNE_zero` 📖	mathematical	—	`Absorbs` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Filter.Eventually` `Set.MapsTo` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`absorbs_iff_eventually_cobounded_mapsTo` `Filter.inv_cobounded₀`
`absorbs_iff_eventually_nhds_zero` 📖	mathematical	`Set` `Set.instMembership` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Absorbs` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Filter.Eventually` `Set.MapsTo` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`nhdsNE_sup_pure` `Filter.eventually_sup` `Filter.eventually_pure` `absorbs_iff_eventually_nhdsNE_zero` `zero_smul`
`absorbs_iff_norm` 📖	mathematical	—	`Absorbs` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `Set` `Set.instHasSubset` `Set.smulSet`	—	`Filter.HasBasis.eventually_iff` `Filter.HasBasis.cobounded_of_norm` `Filter.atTop_basis` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean`
`balanced_empty` 📖	mathematical	—	`Balanced` `Set` `Set.instEmptyCollection`	—	`Set.smul_set_empty` `subset_refl` `Set.instReflSubset`
`balanced_iInter` 📖	mathematical	`Balanced`	`Set.iInter`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.smul_set_iInter_subset` `Set.iInter_mono`
`balanced_iInter₂` 📖	mathematical	`Balanced`	`Set.iInter`	—	`balanced_iInter`
`balanced_iUnion` 📖	mathematical	`Balanced`	`Set.iUnion`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Eq.subset` `Set.instReflSubset` `Set.smul_set_iUnion` `Set.iUnion_mono`
`balanced_iUnion₂` 📖	mathematical	`Balanced`	`Set.iUnion`	—	`balanced_iUnion`
`balanced_iff_closedBall_smul` 📖	mathematical	—	`Balanced` `Set` `Set.instHasSubset` `Set.smul` `Metric.closedBall` `SeminormedRing.toPseudoMetricSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SeminormedRing.toRing` `Real` `Real.instOne`	—	`dist_zero_right`
`balanced_iff_neg_mem` 📖	mathematical	`Convex` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction`	`Balanced` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Set` `Set.instMembership` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Balanced.neg_mem_iff` `NormedDivisionRing.to_normOneClass` `Set.smul_set_subset_iff` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Meta.NormNum.IsRat.to_raw_eq` `Mathlib.Meta.NormNum.isRat_mul` `Mathlib.Meta.NormNum.IsInt.to_isRat` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.IsRat.of_raw` `Mathlib.Meta.NormNum.IsRat.den_nz` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsRat.to_isInt` `Mathlib.Meta.NormNum.isRat_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_add` `add_smul` `neg_smul` `smul_neg` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `sub_nonneg_of_le` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `abs_le` `Real.norm_eq_abs` `zero_le_two` `Real.instZeroLEOneClass` `Mathlib.Tactic.Ring.add_overlap_pf_zero`
`balanced_iff_smul_mem` 📖	mathematical	—	`Balanced` `Set` `Set.instMembership`	—	`Set.smul_set_subset_iff`
`balanced_neg` 📖	mathematical	—	`Balanced` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Set` `Set.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Balanced.neg` `neg_neg`
`balanced_univ` 📖	mathematical	—	`Balanced` `Set.univ`	—	`Set.subset_univ`
`balanced_zero` 📖	mathematical	—	`Balanced` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Set` `Set.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Eq.subset` `Set.instReflSubset` `smul_zero`

---

← Back to Index