Theorem ciSup_mono_of_forall_exists'

Modification history

2026-05-10 00:45
Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
feat(Order/ConditionallyCompleteLattice/Indexed): `ciSup_mono'` for `ConditionallyCompleteLattice` (#38854) …
Added ciSup_mono_of_forall_exists'View on Github →