Commit 2024-09-02 16:21 9a12ff45

View on Github →

feat: ⨅ i, s i < ⊤ ↔ ∃ i, s i < ⊤ (#16320) From LeanAPAP

Estimated changes

added theorem bot_lt_iSup
added theorem iInf_lt_top