Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-23 11:21 5b2c9521

View on Github →

feat(analysis/convex.cone): prove M. Riesz extension theorem, Hahn-Banach theorem (#2120)

  • feat(analysis/convex.cone): prove M. Riesz extension theorem WIP
  • Complete the proof TODO: move many facts to linear_algebra/basic, fix possible build failures in other files
  • Fix compile of analysis/convex/cone
  • Cleanup, rewrite using linear_pmaps
  • Deduce Hahn-Banach theorem from M. Riesz extension theorem
  • Fix lint
  • Apply suggestions from code review [skip_ci] Co-Authored-By: sgouezel
  • Expand comments, prove properties of convex.to_cone.
  • Docstrings
  • Apply suggestions from code review Co-Authored-By: sgouezel
  • Update src/analysis/convex/cone.lean
  • Update src/linear_algebra/basic.lean

Estimated changes

added theorem convex.mem_to_cone'
added theorem convex.mem_to_cone
added theorem convex.subset_to_cone
added def convex.to_cone
added theorem convex.to_cone_eq_Inf
added theorem convex_cone.add_mem
added theorem convex_cone.coe_inf
added theorem convex_cone.comap_id
added theorem convex_cone.convex
added theorem convex_cone.ext'
added theorem convex_cone.ext
added def
added theorem convex_cone.map_id
added theorem convex_cone.map_map
added theorem convex_cone.mem_Inf
added theorem convex_cone.mem_bot
added theorem convex_cone.mem_coe
added theorem convex_cone.mem_comap
added theorem convex_cone.mem_inf
added theorem convex_cone.mem_mk
added theorem convex_cone.mem_top
added theorem convex_cone.smul_mem
added structure convex_cone
added theorem riesz_extension.step
added theorem riesz_extension
added theorem directed.mono
deleted theorem directed_mono
added theorem directed_on.mono
added theorem directed_on_image