Theorems · Theorem · general topology

Metric.IsCover.closure

∀ {X : Type u_1} [inst : PseudoMetricSpace X] {ε : NNReal} {s N : Set X} [ProperSpace X],
  IsClosed N → Metric.IsCover ε s N → Metric.IsCover ε (closure s) N

Alias of the reverse direction of Metric.isCover_closure.

Defined in

Mathlib.Topology.MetricSpace.Cover

Cited by

1 results in Mathlib

Foundations

Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpaceProperSpace