Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-29 21:10 ff352187

View on Github →

feat(analysis/convex/topology): add lemmas (#11615)

Estimated changes

Modified src/analysis/convex/topology.lean

added theorem convex.combo_interior_self_subset_interior

added theorem convex.combo_mem_interior_left

added theorem convex.combo_mem_interior_right

added theorem convex.combo_self_interior_subset_interior

added theorem convex.open_segment_subset_interior_left

added theorem convex.open_segment_subset_interior_right

Modified src/topology/algebra/group.lean

modified theorem is_open.mul_left

Modified src/topology/algebra/ordered/basic.lean

added theorem is_closed.epigraph

added theorem is_closed.hypograph