Commit 2024-07-05 18:40 d225149a

View on Github →

feat(Analysis/Convex): Helly's convexity theorem (#7236)

Prove Helly's convexity theorem (including compact and set versions) and fix typos in Analysis.Convex.Radon
Add alias Set.sInter_mono in the style of Set.sUnion_mono
Mark encard_coe_eq_coe_finsetCard with simp and norm_cast

Estimated changes

Modified Mathlib/Analysis/Convex/Radon.lean

added theorem Convex.helly_theorem'

added theorem Convex.helly_theorem

added theorem Convex.helly_theorem_compact'

added theorem Convex.helly_theorem_compact

added theorem Convex.helly_theorem_set'

added theorem Convex.helly_theorem_set

added theorem Convex.helly_theorem_set_compact'

added theorem Convex.helly_theorem_set_compact

added theorem Convex.radon_partition

deleted theorem radon_partition

Modified Mathlib/Data/Set/Card.lean

modified theorem Set.encard_coe_eq_coe_finsetCard

Modified Mathlib/Data/Set/Lattice.lean