Theorem Set.einfsep_insert_le

Modification history

2023-06-04 14:19

Mathlib/Topology/MetricSpace/Infsep.lean

style: allow `_` for an argument in `notation3` & replace `_foo` with `_` in `notation3` (#4652)

Modified Set.einfsep_insert_le View on Github →

2023-03-04 08:59

Mathlib/Topology/MetricSpace/Infsep.lean

feat: Port Topology.MetricSpace.Infsep (#2613)

Added Set.einfsep_insert_le View on Github →