Theorem ContinuousWithinAt.finset_inf'_apply

Modification history

2023-12-03 09:54
Mathlib/Topology/Order/Lattice.lean
feat(Topology/Order): continuity of `Finset.sup`, `partialSups` etc (#8141) …
Added ContinuousWithinAt.finset_inf'_applyView on Github →