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 ε (closure s) N ↔ Metric.IsCover ε s N)

Defined in

Mathlib.Topology.MetricSpace.Cover

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceProperSpace