Theorem Filter.Tendsto.inf_nhds

Modification history

2024-11-08 16:20
Mathlib/Topology/Order/Lattice.lean
chore: unify binary inf and min (#18707) …
Modified Filter.Tendsto.inf_nhdsView on Github →
2023-12-03 09:54
Mathlib/Topology/Order/Lattice.lean
feat(Topology/Order): continuity of `Finset.sup`, `partialSups` etc (#8141) …
Added Filter.Tendsto.inf_nhdsView on Github →