Theorem Prod.ωSup_zip

Modification history

2025-08-30 02:53
Mathlib/Order/OmegaCompletePartialOrder.lean
chore(Order): golf entire `IsBoundedUnder.eventually_le` and `ωSup_zip` using `tauto` and `rfl` (#28568)
Modified Prod.ωSup_zipView on Github →
2023-01-20 07:27
Mathlib/Order/OmegaCompletePartialOrder.lean
feat: port Order.OmegaCompletePartialOrder (#1168) …
Added Prod.ωSup_zipView on Github →