Commit 2024-01-11 10:24 33a5585b

View on Github →

feat: two lemmas about partial homeomorphisms (#9623) From sphere-eversion. While I'm in the area,

  • remove image_isOpen_of_isOpen, which is an exact duplicate of isOpen_image_of_subset_source
  • rename image_isOpen_of_isOpen' to isOpen_image_source_inter_of_isOpen (which matches the naming convention)
  • move isOpen_inter_preimage_symm next to its adjacent lemmas

Estimated changes