Commit 2023-04-24 21:32 0993683f

View on Github →

feat: port Analysis.Convex.Topology (#3624)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Topology.lean

added theorem Convex.add_smul_mem_interior'

added theorem Convex.add_smul_mem_interior

added theorem Convex.add_smul_sub_mem_interior'

added theorem Convex.add_smul_sub_mem_interior

added theorem Convex.closure_subset_image_homothety_interior_of_one_lt

added theorem Convex.closure_subset_interior_image_homothety_of_one_lt

added theorem Convex.combo_closure_interior_mem_interior

added theorem Convex.combo_closure_interior_subset_interior

added theorem Convex.combo_interior_closure_mem_interior

added theorem Convex.combo_interior_closure_subset_interior

added theorem Convex.combo_interior_self_mem_interior

added theorem Convex.combo_interior_self_subset_interior

added theorem Convex.combo_self_interior_mem_interior

added theorem Convex.combo_self_interior_subset_interior

added theorem Convex.openSegment_closure_interior_subset_interior

added theorem Convex.openSegment_interior_closure_subset_interior

added theorem Convex.openSegment_interior_self_subset_interior

added theorem Convex.openSegment_self_interior_subset_interior

added theorem Convex.subset_interior_image_homothety_of_one_lt

added theorem Real.convex_iff_isPreconnected

added theorem Set.Finite.isClosed_convexHull

added theorem Set.Finite.isCompact_convexHull

added theorem bounded_stdSimplex

added theorem closure_openSegment

added theorem isClosed_stdSimplex

added theorem isCompact_stdSimplex

added theorem segment_subset_closure_openSegment

added theorem stdSimplex_subset_closedBall