BalancedCoreHull

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

Statistics

Metric	Count
Definitions balancedCore, balancedCoreAux, balancedHull	3
Theorems balancedCore_eq, balancedHull_subset_of_subset, subset_balancedCore_of_subset, zero_mem, balancedCore, balancedCoreAux_balanced, balancedCoreAux_empty, balancedCoreAux_maximal, balancedCoreAux_subset, balancedCore_balanced, balancedCore_empty, balancedCore_eq_iInter, balancedCore_mem_nhds_zero, balancedCore_nonempty_iff, balancedCore_subset, balancedCore_subset_balancedCoreAux, balancedCore_zero_mem, balanced, balancedHull_add_subset, balancedHull_mono, mem_balancedCoreAux_iff, mem_balancedCore_iff, mem_balancedHull_iff, nhds_basis_balanced, nhds_basis_closed_balanced, smul_balancedCore_subset, subset_balancedCore, subset_balancedHull	28
Total	31

Balanced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
balancedCore_eq 📖	mathematical	Balanced	balancedCore	—	le_antisymm balancedCore_subset subset_balancedCore_of_subset subset_rfl Set.instReflSubset
balancedHull_subset_of_subset 📖	mathematical	Balanced Set Set.instHasSubset	balancedHull	—	mem_balancedHull_iff smul_mem
subset_balancedCore_of_subset 📖	mathematical	Balanced Set Set.instHasSubset	balancedCore	—	Set.subset_sUnion_of_mem
zero_mem 📖	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.Nonempty	Set Set.instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	balancedCore_nonempty_iff balancedCore_eq

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
balancedCore 📖	mathematical	—	IsClosed balancedCore 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	—	balancedCore_eq_iInter isClosed_iInter lt_of_lt_of_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing isClosedMap_smul_of_ne_zero ContinuousSMul.continuousConstSMul norm_pos_iff Mathlib.Tactic.Contrapose.contrapose₂ balancedCore_nonempty_iff isClosed_empty

(root)

Definitions

Name	Category	Theorems
balancedCore 📖	CompOp	14 math math: smul_balancedCore_subset, balancedCore_nonempty_iff, balancedCore_mem_nhds_zero, subset_balancedCore, Balanced.balancedCore_eq, balancedCore_empty, IsClosed.balancedCore, balancedCore_balanced, balancedCore_zero_mem, mem_balancedCore_iff, balancedCore_subset, balancedCore_eq_iInter, Balanced.subset_balancedCore_of_subset, balancedCore_subset_balancedCoreAux
balancedCoreAux 📖	CompOp	5 math math: balancedCoreAux_maximal, mem_balancedCoreAux_iff, balancedCoreAux_subset, balancedCoreAux_empty, balancedCore_subset_balancedCoreAux
balancedHull 📖	CompOp	9 math math: balancedHull_subset_convexHull_union_neg, subset_balancedHull, balancedHull_add_subset, mem_balancedHull_iff, Balanced.balancedHull_subset_of_subset, absConvexHull_eq_convexHull_balancedHull, balancedHull.balanced, balancedHull_mono, balancedHull_convexHull_subseteq_absConvexHull

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
balancedCoreAux_balanced 📖	mathematical	Set Set.instMembership balancedCoreAux 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 NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Balanced	—	eq_or_ne zero_smul mem_balancedCoreAux_iff norm_smul NormMulClass.toNormSMulClass NormedDivisionRing.toNormMulClass norm_inv one_le_mul_of_one_le_of_one_le Real.instZeroLEOneClass IsOrderedRing.toPosMulMono Real.instIsOrderedRing one_le_inv₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing norm_pos_iff Set.mem_inv_smul_set_iff₀ smul_assoc Set.isScalarTower IsScalarTower.left
balancedCoreAux_empty 📖	mathematical	—	balancedCoreAux 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.instEmptyCollection	—	Set.smul_set_empty Eq.ge NormOneClass.norm_one NormedDivisionRing.to_normOneClass Set.notMem_empty
balancedCoreAux_maximal 📖	mathematical	Set Set.instHasSubset 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	balancedCoreAux	—	mem_balancedCoreAux_iff Set.mem_smul_set_iff_inv_smul_mem₀ norm_pos_iff LT.lt.trans_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Balanced.smul_mem norm_inv inv_le_one_of_one_le₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono
balancedCoreAux_subset 📖	mathematical	—	Set Set.instHasSubset balancedCoreAux 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	—	one_smul mem_balancedCoreAux_iff Eq.ge NormOneClass.norm_one NormedDivisionRing.to_normOneClass
balancedCore_balanced 📖	mathematical	—	Balanced balancedCore	—	smul_balancedCore_subset
balancedCore_empty 📖	mathematical	—	balancedCore Set Set.instEmptyCollection	—	Set.eq_empty_of_subset_empty balancedCore_subset
balancedCore_eq_iInter 📖	mathematical	Set Set.instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	balancedCore 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.iInter Real Real.instLE Real.instOne Norm.norm NormedDivisionRing.toNorm Set.smulSet	—	HasSubset.Subset.antisymm Set.instAntisymmSubset balancedCore_subset_balancedCoreAux Balanced.subset_balancedCore_of_subset balancedCoreAux_balanced balancedCore_zero_mem balancedCoreAux_subset
balancedCore_mem_nhds_zero 📖	mathematical	Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	balancedCore 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	—	Continuous.tendsto' ContinuousSMul.continuous_smul smul_zero Filter.Tendsto.basis_left Filter.HasBasis.prod_nhds NormedAddCommGroup.nhds_zero_basis_norm_lt Filter.basis_sets Filter.nonempty_of_mem Filter.HasBasis.mem_of_mem nhdsWithin_hasBasis set_smul_mem_nhds_zero_iff ContinuousSMul.continuousConstSMul Filter.mem_of_superset subset_balancedCore mem_of_mem_nhds smul_smul norm_mul NormedDivisionRing.toNormMulClass one_mul mul_lt_mul' IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg one_pos Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero
balancedCore_nonempty_iff 📖	mathematical	—	Set.Nonempty balancedCore 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.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Set.zero_subset HasSubset.Subset.trans Set.instIsTransSubset Eq.superset Set.instReflSubset Set.zero_smul_set balancedCore_balanced Eq.trans_le norm_zero zero_le_one Real.instZeroLEOneClass balancedCore_subset balancedCore_zero_mem
balancedCore_subset 📖	mathematical	—	Set Set.instHasSubset balancedCore	—	Set.sUnion_subset
balancedCore_subset_balancedCoreAux 📖	mathematical	—	Set Set.instHasSubset balancedCore 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 balancedCoreAux	—	balancedCoreAux_maximal balancedCore_subset balancedCore_balanced
balancedCore_zero_mem 📖	mathematical	Set Set.instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	balancedCore 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	—	mem_balancedCore_iff balanced_zero Set.zero_subset Set.zero_mem_zero
balancedHull_add_subset 📖	mathematical	—	Set Set.instHasSubset balancedHull 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.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Balanced.balancedHull_subset_of_subset Balanced.add balancedHull.balanced Set.add_subset_add subset_balancedHull
balancedHull_mono 📖	mathematical	Set Set.instHasSubset	balancedHull	—	mem_balancedHull_iff Set.smul_set_mono
mem_balancedCoreAux_iff 📖	mathematical	—	Set Set.instMembership balancedCoreAux Set.smulSet	—	Set.mem_iInter₂
mem_balancedCore_iff 📖	mathematical	—	Set Set.instMembership balancedCore Balanced Set.instHasSubset	—	—
mem_balancedHull_iff 📖	mathematical	—	Set Set.instMembership balancedHull Real Real.instLE Norm.norm SeminormedRing.toNorm Real.instOne Set.smulSet	—	—
nhds_basis_balanced 📖	mathematical	—	Filter.HasBasis Set nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Filter Filter.instMembership 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	—	Filter.hasBasis_self balancedCore_mem_nhds_zero balancedCore_balanced balancedCore_subset
nhds_basis_closed_balanced 📖	mathematical	—	Filter.HasBasis Set nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Filter Filter.instMembership IsClosed 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	—	Filter.HasBasis.to_hasBasis closed_nhds_basis balancedCore_mem_nhds_zero IsClosed.balancedCore balancedCore_balanced balancedCore_subset Eq.subset Set.instReflSubset
smul_balancedCore_subset 📖	mathematical	Real Real.instLE Norm.norm SeminormedRing.toNorm Real.instOne	Set Set.instHasSubset Set.smulSet balancedCore	—	mem_balancedCore_iff Set.smul_mem_smul_set
subset_balancedCore 📖	mathematical	Set Set.instMembership NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set.instHasSubset Set.smulSet 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	balancedCore NormedRing.toSeminormedRing NormedDivisionRing.toNormedRing	—	balancedCore_eq_iInter Set.subset_iInter₂ Set.subset_smul_set_iff₀ norm_pos_iff LT.lt.trans_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing norm_inv inv_le_one_of_one_le₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono
subset_balancedHull 📖	mathematical	—	Set Set.instHasSubset balancedHull 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	—	mem_balancedHull_iff Eq.le NormOneClass.norm_one one_smul

balancedHull

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
balanced 📖	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 balancedHull	—	Set.smul_set_iUnion₂ LE.le.trans norm_mul_le mul_le_one₀ IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg smul_assoc Set.isScalarTower IsScalarTower.left

---

← Back to Index