Commit 2023-05-24 09:57 56ebf4cc

View on Github →

feat: port Analysis.LocallyConvex.WithSeminorms (#4170)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

added theorem Inducing.withSeminorms

added theorem LinearMap.withSeminorms_induced

added theorem NormedSpace.toLocallyConvexSpace'

added def Seminorm.IsBounded

added theorem Seminorm.const_isBounded

added theorem Seminorm.cont_normedSpace_to_withSeminorms

added theorem Seminorm.cont_withSeminorms_normedSpace

added theorem Seminorm.continuous_from_bounded

added theorem Seminorm.continuous_iff_continuous_comp

added theorem Seminorm.continuous_of_continuous_comp

added theorem Seminorm.isBounded_const

added theorem Seminorm.isBounded_sup

added def SeminormFamily.basisSets

added theorem SeminormFamily.basisSets_add

added theorem SeminormFamily.basisSets_iff

added theorem SeminormFamily.basisSets_intersect

added theorem SeminormFamily.basisSets_mem

added theorem SeminormFamily.basisSets_neg

added theorem SeminormFamily.basisSets_nonempty

added theorem SeminormFamily.basisSets_singleton_mem

added theorem SeminormFamily.basisSets_smul

added theorem SeminormFamily.basisSets_smul_left

added theorem SeminormFamily.basisSets_smul_right

added theorem SeminormFamily.basisSets_zero

added def SeminormFamily.comp

added theorem SeminormFamily.comp_apply

added theorem SeminormFamily.filter_eq_iInf

added theorem SeminormFamily.finset_sup_comp

added theorem SeminormFamily.withSeminorms_iff_nhds_eq_iInf

added theorem SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf

added theorem SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInf

added theorem SeminormFamily.withSeminorms_of_hasBasis

added theorem SeminormFamily.withSeminorms_of_nhds

added theorem WithSeminorms.T1_of_separating

added theorem WithSeminorms.continuous_seminorm

added theorem WithSeminorms.first_countable

added theorem WithSeminorms.hasBasis

added theorem WithSeminorms.hasBasis_ball

added theorem WithSeminorms.hasBasis_zero_ball

added theorem WithSeminorms.image_isVonNBounded_iff_finset_seminorm_bounded

added theorem WithSeminorms.image_isVonNBounded_iff_seminorm_bounded

added theorem WithSeminorms.isOpen_iff_mem_balls

added theorem WithSeminorms.isVonNBounded_iff_finset_seminorm_bounded

added theorem WithSeminorms.isVonNBounded_iff_seminorm_bounded

added theorem WithSeminorms.mem_nhds_iff

added theorem WithSeminorms.separating_iff_T1

added theorem WithSeminorms.separating_of_T1

added theorem WithSeminorms.tendsto_nhds'

added theorem WithSeminorms.tendsto_nhds

added theorem WithSeminorms.tendsto_nhds_atTop

added theorem WithSeminorms.toLocallyConvexSpace

added theorem WithSeminorms.topologicalAddGroup

added theorem WithSeminorms.withSeminorms_eq

added structure WithSeminorms

added theorem norm_withSeminorms

Modified Mathlib/Analysis/Normed/Group/Basic.lean