Commit 2023-05-25 08:46 b4ae759d

View on Github →

feat: port Analysis.LocallyConvex.AbsConvex (#4320)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/LocallyConvex/AbsConvex.lean

added theorem AbsConvexOpenSets.coe_balanced

added theorem AbsConvexOpenSets.coe_convex

added theorem AbsConvexOpenSets.coe_isOpen

added theorem AbsConvexOpenSets.coe_nhds

added theorem AbsConvexOpenSets.coe_zero_mem

added def AbsConvexOpenSets

added theorem gaugeSeminormFamily_ball

added theorem nhds_basis_abs_convex

added theorem nhds_basis_abs_convex_open

added theorem with_gaugeSeminormFamily