Commit 2021-01-10 19:12 cc6f039f

View on Github →

feat(equiv|set|topology): various additions (#5656) define sigma_compact_space update module doc for topology/subset_properties define shearing some lemmas in set.basic, equiv.mul_add and topology.instances.ennreal

Estimated changes

Modified src/data/equiv/basic.lean

added def equiv.prod_shear

Modified src/data/equiv/mul_add.lean

added theorem equiv.mul_left_symm_apply

added theorem equiv.mul_right_symm_apply

Modified src/data/set/basic.lean

added theorem set.mk_preimage_prod

added theorem set.mk_preimage_prod_left_fn_eq_if

added theorem set.mk_preimage_prod_right_fn_eq_if

added theorem set.prod_preimage_left

added theorem set.prod_preimage_right

Modified src/topology/algebra/group.lean

added theorem homeomorph.shear_mul_right_coe

added theorem homeomorph.shear_mul_right_symm_coe

Modified src/topology/instances/ennreal.lean

added theorem ennreal.supr_eq_zero

Modified src/topology/subset_properties.lean

added theorem Union_compact_covering

added def compact_covering

added theorem is_compact_compact_covering