Commit 2021-12-08 15:28 678566f2

View on Github →

feat(topology/algebra/group): Addition of interiors (#10659) This proves interior s * t ⊆ interior (s * t), a few prerequisites, and generalizes to is_open.mul_left/is_open.mul_right.

Estimated changes

Modified src/algebra/pointwise.lean

added theorem set.mul_subset_mul_left

added theorem set.mul_subset_mul_right

Modified src/data/set/basic.lean

added theorem set.image2_subset_left

added theorem set.image2_subset_right

modified theorem set.image_preimage_subset

modified theorem set.inclusion_self

Modified src/topology/algebra/group.lean

added theorem is_closed.inv

added theorem is_open.inv

modified theorem is_open.mul_left

modified theorem is_open.mul_right

added theorem subset_interior_mul

added theorem subset_interior_mul_left

added theorem subset_interior_mul_right