Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-25 06:24 7d64215f

View on Github →

chore(analysis/convex/topology): generalize a few lemmas (#13656) This way they work for 𝕜 = ℚ too.

Estimated changes

Modified src/analysis/convex/topology.lean

modified theorem convex.add_smul_mem_interior'

modified theorem convex.add_smul_mem_interior

modified theorem convex.add_smul_sub_mem_interior'

modified theorem convex.add_smul_sub_mem_interior

modified theorem convex.combo_closure_interior_mem_interior

modified theorem convex.combo_closure_interior_subset_interior

modified theorem convex.combo_interior_closure_mem_interior

modified theorem convex.combo_interior_closure_subset_interior

modified theorem convex.combo_interior_self_mem_interior

modified theorem convex.combo_interior_self_subset_interior

modified theorem convex.combo_self_interior_mem_interior

modified theorem convex.combo_self_interior_subset_interior

modified theorem convex.open_segment_closure_interior_subset_interior

modified theorem convex.open_segment_interior_closure_subset_interior

modified theorem convex.open_segment_interior_self_subset_interior

modified theorem convex.open_segment_self_interior_subset_interior