Commit 2025-08-30 02:53 d9686a36

View on Github →

chore(Order): golf entire IsBoundedUnder.eventually_le and ωSup_zip using tauto and rfl (#28568)

Estimated changes

modified theorem Prod.ωSup_zip