Add lower bound lemma for finite sets

Forked off from the discussion here: lambda-rust!38 (comment 104108)

This adds a variant of minimal_exists which does not require the set to be non-empty, but in return also does not guarantee that the element is part of the set.

I'm not sure what the best naming for this lemma is. Maybe it should be called infimum_exists instead of lower_bound_exists? Should it be prefixed by set, like many other lemmas in the file for which it is not directly clear it's related to sets? (and should minimal_exists be prefixed accordingly?)

mentioned in merge request lambda-rust!38 (merged)

added 1 commit

• b8047957 - revert accidental change

Compare with previous version

Thanks.

I'm not sure what the best naming for this lemma is. Maybe it should be called infimum_exists instead of lower_bound_exists?

No strong opinion.

Should it be prefixed by set, like many other lemmas in the file for which it is not directly clear it's related to sets? (and should minimal_exists be prefixed accordingly?)

The convention is a bit messy, so it's not clear. I wouldn't change the other lemma now, since the definition minimal already does not have a set_ prefix. The proposed name does not involve minimal, so it's less clear whether to include set_ or not. I don't have a strong opinion.

minimal_exists would be a good name for the new lemma. Should we rename the old one?

added 1 commit

• 36b7a08f - rename; add changelog

Compare with previous version

added 1 commit

• d1ae5165 - fix script

Compare with previous version

added 3 commits

• d1ae5165...84d04958 - 2 commits from branch master
• b8660df8 - Add lower bound lemma for finite sets

Compare with previous version

added 1 commit

• 7453c90b - newline

Compare with previous version

resolved all threads

added 1 commit

• c5d206d5 - fix changelog

Compare with previous version

resolved all threads

LGTM, thanks! I'll take care of updating dependencies that use the old lemma name.

mentioned in commit 8548ce42

merged

@iris-users this renames a lemma, you may have to run a sed script to update your proofs:

• Rename minimal_exists to minimal_exists_elem_of and minimal_exists_L to minimal_exists_elem_of_L.