Documentation Verification Report

LocallyConvex

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

Statistics

Metric	Count
Definitions `LocallyConvexSpace`	1
Theorems `eventually_nhdsWithin_segment`, `locPathConnectedSpace`, `exists_open_convexes`, `toLocallyConvexSpace`, `convex_basis`, `convex_basis_zero`, `convex_open_basis_zero`, `iInf`, `induced`, `inf`, `ofBases`, `ofBasisZero`, `sInf`, `toLocPathConnectedSpace`, `locallyConvexSpace`, `locallyConvexSpace`, `locallyConvexSpace`, `exists_open_convex_of_notMem`, `instLocallyConvexSpaceSubtypeMemSubmodule`, `locallyConvexSpace_iff`, `locallyConvexSpace_iff_exists_convex_subset`, `locallyConvexSpace_iff_exists_convex_subset_zero`, `locallyConvexSpace_iff_zero`	23
Total	24

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_nhdsWithin_segment` 📖	—	`Convex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Set` `Set.instMembership` `Filter.Eventually` `nhdsWithin`	—	—	`eventually_nhdsWithin_iff` `Filter.HasBasis.eventually_iff` `LocallyConvexSpace.convex_basis` `segment_subset` `mem_of_mem_nhds`
`locPathConnectedSpace` 📖	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`	`LocPathConnectedSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`mem_nhds_subtype` `Filter.HasBasis.mem_iff` `LocallyConvexSpace.convex_basis` `ContinuousAt.preimage_mem_nhds` `continuousAt_subtype_val` `IsPathConnected.preimage_coe` `isPathConnected` `IsTopologicalAddGroup.toContinuousAdd` `inter` `mem_of_mem_nhds` `Set.inter_subset_left` `Subtype.preimage_coe_self_inter` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.preimage_mono` `Filter.mem_of_superset`

Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_open_convexes` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Convex` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsCompact`	`IsOpen` `Set.instHasSubset`	—	`Filter.HasBasis.comap` `LocallyConvexSpace.convex_open_basis_zero` `exists_uniform_thickening_of_basis` `uniformity_eq_comap_nhds_zero` `IsUniformAddGroup.isRightUniformAddGroup` `isUniformAddGroup_of_addCommGroup` `IsOpen.add_left` `VAddCommClass.continuousConstVAdd` `vaddCommClass_self` `IsTopologicalAddGroup.toContinuousAdd` `Convex.add` `Set.subset_add_left` `Set.iUnion_congr_Prop` `Set.image_add_left` `sub_eq_neg_add`

LinearOrderedSemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toLocallyConvexSpace` 📖	mathematical	—	`LocallyConvexSpace` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`isBot_or_exists_lt` `SemilatticeInf.instIsCodirectedOrder` `Filter.HasBasis.to_hasBasis'` `nhds_bot_basis` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule` `Set.Subset.rfl` `isTop_or_exists_gt` `SemilatticeSup.instIsDirectedOrder` `nhds_top_basis` `instNoTopOrderOfNoMaxOrder` `IsStrictOrderedRing.toNoMaxOrder` `subset_rfl` `Set.instReflSubset` `nhds_basis_Ioo'`

LocallyConvexSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convex_basis` 📖	mathematical	—	`Filter.HasBasis` `Set` `nhds` `Filter` `Filter.instMembership` `Convex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—
`convex_basis_zero` 📖	mathematical	—	`Filter.HasBasis` `Set` `nhds` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Filter` `Filter.instMembership` `Convex` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`convex_basis`
`convex_open_basis_zero` 📖	mathematical	—	`Filter.HasBasis` `Set` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set.instMembership` `IsOpen` `Convex` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`Filter.HasBasis.to_hasBasis` `convex_basis_zero` `mem_interior_iff_mem_nhds` `isOpen_interior` `Convex.interior` `IsStrictOrderedRing.toZeroLEOneClass` `interior_subset` `IsOpen.mem_nhds` `subset_rfl` `Set.instReflSubset`
`iInf` 📖	mathematical	`LocallyConvexSpace`	`iInf` `TopologicalSpace` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice`	—	`sInf` `Set.forall_mem_range`
`induced` 📖	mathematical	—	`LocallyConvexSpace` `TopologicalSpace.induced` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	`ofBases` `nhds_induced` `Filter.HasBasis.comap` `convex_basis` `Convex.linear_preimage`
`inf` 📖	mathematical	—	`LocallyConvexSpace` `TopologicalSpace` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice`	—	`inf_eq_iInf` `iInf`
`ofBases` 📖	mathematical	`Filter.HasBasis` `nhds` `Convex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`LocallyConvexSpace`	—	`Filter.HasBasis.to_hasBasis` `Filter.HasBasis.mem_of_mem` `le_refl` `Filter.HasBasis.property_index` `Filter.HasBasis.set_index_subset`
`ofBasisZero` 📖	mathematical	`Filter.HasBasis` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Convex` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`LocallyConvexSpace`	—	`ofBases` `map_add_left_nhds_zero` `Filter.HasBasis.map` `Convex.translate`
`sInf` 📖	mathematical	`LocallyConvexSpace`	`InfSet.sInf` `TopologicalSpace` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice`	—	`ofBases` `nhds_sInf` `iInf_subtype''` `Filter.HasBasis.iInf'` `locallyConvexSpace_iff` `convex_iInter`
`toLocPathConnectedSpace` 📖	mathematical	—	`LocPathConnectedSpace`	—	`LocPathConnectedSpace.of_bases` `convex_basis` `Convex.isPathConnected` `IsTopologicalAddGroup.toContinuousAdd` `Set.nonempty_of_mem` `mem_of_mem_nhds`

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`locallyConvexSpace` 📖	mathematical	`LocallyConvexSpace`	`addCommMonoid` `module` `topologicalSpace`	—	`LocallyConvexSpace.iInf` `LocallyConvexSpace.induced`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`locallyConvexSpace` 📖	mathematical	—	`LocallyConvexSpace` `instAddCommMonoid` `instModule` `instTopologicalSpaceProd`	—	`LocallyConvexSpace.inf` `LocallyConvexSpace.induced`

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`locallyConvexSpace` 📖	mathematical	`Topology.IsInducing` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`LocallyConvexSpace`	—	`eq_induced` `LocallyConvexSpace.induced`

(root)

Definitions

Name	Category	Theorems
`LocallyConvexSpace` 📖	CompData	25 math math: `WithSeminorms.toLocallyConvexSpace`, `LocallyConvexSpace.inf`, `locallyConvexSpace_iff`, `Topology.IsInducing.locallyConvexSpace`, `PointwiseConvergenceCLM.instLocallyConvexSpace`, `ContinuousLinearMapWOT.instLocallyConvexSpace`, `ContinuousLinearMap.instLocallyConvexSpace`, `Prod.locallyConvexSpace`, `instLocallyConvexSpaceSubtypeMemSubmodule`, `LocallyConvexSpace.ofBases`, `ContDiffMapSupportedIn.locallyConvexSpace`, `WeakBilin.locallyConvexSpace`, `SchwartzMap.instLocallyConvexSpace`, `NormedSpace.toLocallyConvexSpace`, `ContinuousMap.instLocallyConvexSpace`, `LocallyConvexSpace.induced`, `TestFunction.instLocallyConvexSpaceReal`, `LocallyConvexSpace.ofBasisZero`, `LinearOrderedSemiring.toLocallyConvexSpace`, `instLocallyConvexSpaceRealOfPolynormableSpace`, `locallyConvexSpace_iff_zero`, `NormedSpace.toLocallyConvexSpace'`, `UniformConvergenceCLM.locallyConvexSpace`, `locallyConvexSpace_iff_exists_convex_subset_zero`, `locallyConvexSpace_iff_exists_convex_subset`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_open_convex_of_notMem` 📖	mathematical	`Set` `Set.instMembership` `Convex` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`IsOpen` `Set.instHasSubset` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`Disjoint.exists_open_convexes`
`instLocallyConvexSpaceSubtypeMemSubmodule` 📖	mathematical	—	`LocallyConvexSpace` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `instTopologicalSpaceSubtype`	—	`Topology.IsInducing.locallyConvexSpace` `Topology.IsInducing.subtypeVal`
`locallyConvexSpace_iff` 📖	mathematical	—	`LocallyConvexSpace` `Filter.HasBasis` `Set` `nhds` `Filter` `Filter.instMembership` `Convex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`LocallyConvexSpace.convex_basis`
`locallyConvexSpace_iff_exists_convex_subset` 📖	mathematical	—	`LocallyConvexSpace` `Set` `Filter` `Filter.instMembership` `nhds` `Convex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Set.instHasSubset`	—	`locallyConvexSpace_iff` `Filter.hasBasis_self`
`locallyConvexSpace_iff_exists_convex_subset_zero` 📖	mathematical	—	`LocallyConvexSpace` `AddCommGroup.toAddCommMonoid` `Set` `Filter` `Filter.instMembership` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Convex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Set.instHasSubset`	—	`locallyConvexSpace_iff_zero` `Filter.hasBasis_self`
`locallyConvexSpace_iff_zero` 📖	mathematical	—	`LocallyConvexSpace` `AddCommGroup.toAddCommMonoid` `Filter.HasBasis` `Set` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Filter` `Filter.instMembership` `Convex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`LocallyConvexSpace.convex_basis` `LocallyConvexSpace.ofBasisZero`

---

← Back to Index