Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-10 09:05 d70e26bf

View on Github →

feat(analysis/convex/topology): improve some lemmas (#13136) Replace some s with closure s in the LHS of ⊆ in some lemmas.

Estimated changes

Modified src/analysis/calculus/fderiv_symmetric.lean

Modified src/analysis/convex/integral.lean

Modified src/analysis/convex/strict_convex_space.lean

Modified src/analysis/convex/topology.lean

added theorem convex.add_smul_mem_interior'

added theorem convex.add_smul_sub_mem_interior'

deleted theorem convex.closure

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

deleted theorem convex.combo_mem_interior_left

deleted theorem convex.combo_mem_interior_right

added theorem convex.combo_self_interior_mem_interior

deleted theorem convex.interior

deleted theorem convex.is_path_connected

added theorem convex.open_segment_closure_interior_subset_interior

added theorem convex.open_segment_interior_closure_subset_interior

added theorem convex.open_segment_interior_self_subset_interior

added theorem convex.open_segment_self_interior_subset_interior

deleted theorem convex.open_segment_subset_interior_left

deleted theorem convex.open_segment_subset_interior_right

modified theorem convex.subset_interior_image_homothety_of_one_lt

deleted theorem topological_add_group.path_connected