Commit 2023-12-01 16:02 8b8aaa21
View on Github →chore: rename lemmas containing "of_open" to match the naming convention (#8229) Mostly, this means replacing "of_open" by "of_isOpen". A few lemmas names were misleading and are corrected differently. Zulip discussion.