Theorem isGLB_congr

Modification history

2026-01-16 12:21
Mathlib/Order/Bounds/Basic.lean
feat(Order/Bounds/Basic): use `to_dual` - part 1 (#33760) …
Deleted isGLB_congrView on Github →
2025-01-22 19:43
Mathlib/Order/Bounds/Basic.lean
feat(Order/Bounds/Lattice): bounds over collections of sets (#19150) …
Added isGLB_congrView on Github →