Commit 2023-04-10 18:08 5127295b

View on Github →

feat: port Analysis.LocallyConvex.Polar (#3367)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/LocallyConvex/Polar.lean

added def LinearMap.polar

added theorem LinearMap.polar_antitone

added theorem LinearMap.polar_empty

added theorem LinearMap.polar_eq_interᵢ

added theorem LinearMap.polar_gc

added theorem LinearMap.polar_mem

added theorem LinearMap.polar_mem_iff

added theorem LinearMap.polar_union

added theorem LinearMap.polar_unionᵢ

added theorem LinearMap.polar_univ

added theorem LinearMap.polar_weak_closed

added theorem LinearMap.polar_zero

added theorem LinearMap.subset_bipolar

added theorem LinearMap.tripolar_eq_polar

added theorem LinearMap.zero_mem_polar