Documentation Verification Report

AbsConvexOpen

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

Statistics

Metric	Count
Definitions `AbsConvexOpenSets`, `instCoeOut`, `gaugeSeminormFamily`	3
Theorems `coe_balanced`, `coe_convex`, `coe_isOpen`, `coe_nhds`, `coe_zero_mem`, `instNonempty`, `toPolynormableSpace`, `gaugeSeminormFamily_ball`, `with_gaugeSeminormFamily`	9
Total	12

AbsConvexOpenSets

Definitions

Name	Category	Theorems
`instCoeOut` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_balanced` 📖	mathematical	—	`Balanced` `Set` `Set.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `IsOpen` `AbsConvex`	—	—
`coe_convex` 📖	mathematical	—	`Convex` `Ring.toSemiring` `SeminormedRing.toRing` `Set` `Set.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `IsOpen` `AbsConvex`	—	—
`coe_isOpen` 📖	mathematical	—	`IsOpen` `Set` `Set.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AbsConvex`	—	—
`coe_nhds` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Set.instMembership` `IsOpen` `AbsConvex`	—	`IsOpen.mem_nhds` `coe_isOpen` `coe_zero_mem`
`coe_zero_mem` 📖	mathematical	—	`Set` `Set.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `IsOpen` `AbsConvex`	—	—
`instNonempty` 📖	mathematical	—	`AbsConvexOpenSets`	—	`exists_true_iff_nonempty` `Set.mem_univ` `isOpen_univ` `balanced_univ` `convex_univ`

LocallyConvexSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toPolynormableSpace` 📖	mathematical	—	`PolynormableSpace` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField`	—	`WithSeminorms.toPolynormableSpace` `with_gaugeSeminormFamily`

(root)

Definitions

Name	Category	Theorems
`AbsConvexOpenSets` 📖	CompOp	2 math math: `with_gaugeSeminormFamily`, `AbsConvexOpenSets.instNonempty`
`gaugeSeminormFamily` 📖	CompOp	2 math math: `with_gaugeSeminormFamily`, `gaugeSeminormFamily_ball`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gaugeSeminormFamily_ball` 📖	mathematical	—	`Seminorm.ball` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `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` `gaugeSeminormFamily` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Real` `Real.instOne` `Set` `Set.instMembership` `AddCommMonoid.toAddMonoid` `IsOpen` `AbsConvex` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RCLike.toPartialOrder`	—	`Seminorm.ball_zero_eq` `gauge_lt_one_eq_self_of_isOpen` `Convex.lift` `RCLike.toZeroLEOneClass` `PosSMulMono.toSMulPosMono` `Real.instIsOrderedRing` `RCLike.toIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `instIsOrderedModule` `RCLike.toStarOrderedRing` `RCLike.instStarModuleReal` `IsScalarTower.right` `Algebra.to_smulCommClass` `AbsConvexOpenSets.coe_convex` `AbsConvexOpenSets.coe_zero_mem` `AbsConvexOpenSets.coe_isOpen`
`with_gaugeSeminormFamily` 📖	mathematical	—	`WithSeminorms` `AbsConvexOpenSets` `AddCommGroup.toAddCommMonoid` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `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` `RCLike.toPartialOrder` `gaugeSeminormFamily`	—	`SeminormFamily.withSeminorms_of_hasBasis` `Filter.HasBasis.to_hasBasis` `nhds_hasBasis_absConvex_open` `RCLike.toZeroLEOneClass` `gaugeSeminormFamily_ball` `SeminormFamily.basisSets_singleton_mem` `one_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Eq.subset` `Set.instReflSubset` `SeminormFamily.basisSets_iff` `Seminorm.ball_finset_sup_eq_iInter` `Set.mem_iInter₂` `sub_self` `map_zero` `AddGroupSeminormClass.toZeroHomClass` `SeminormClass.toAddGroupSeminormClass` `Seminorm.instSeminormClass` `isOpen_biInter_finset` `norm_algebraMap'` `NormedDivisionRing.to_normOneClass` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_one` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `LT.lt.ne'` `Seminorm.smul_ball_zero` `IsOpen.smul₀` `ContinuousSMul.continuousConstSMul` `AbsConvexOpenSets.coe_isOpen` `balanced_iInter₂` `Seminorm.balanced_ball_zero` `convex_iInter₂` `convex_of_nonneg_surjective_algebraMap` `instFaithfulSMul_1` `RCLike.nonneg_iff_exists_ofReal` `Seminorm.convex_ball`

---

← Back to Index