Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • S stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 79
    • Issues 79
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 16
    • Merge requests 16
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • stdpp
  • Merge requests
  • !335

Add lemma `map_subseteq_inv`.

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Robbert Krebbers requested to merge robbert/map_subseteq_inv into master Nov 18, 2021
  • Overview 2
  • Commits 1
  • Pipelines 1
  • Changes 1

As pointed out by @swils in https://mattermost.mpi-sws.org/iris/pl/wzsucg5swtrttqhsawdd8pzama this lemma is missing

It's all the way down the file since I need properties of ∖. If someone knows a (short) proof without, we can move the property up, closer towards other properties on the order.

Edited Nov 22, 2021 by Robbert Krebbers
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: robbert/map_subseteq_inv