Theorem lowerBounds_mono_of_isCoinitialFor

Modification history

2026-01-16 12:21
Mathlib/Order/Bounds/Basic.lean
feat(Order/Bounds/Basic): use `to_dual` - part 1 (#33760) …
Deleted lowerBounds_mono_of_isCoinitialForView on Github →
2025-05-07 09:33
Mathlib/Order/Bounds/Basic.lean
feat(Order): directed products and upper bounds (#21493) …
Added lowerBounds_mono_of_isCoinitialForView on Github →