Theorems · Theorem · general topology

AntilipschitzWith.isComplete_range

∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β}
  [CompleteSpace α], AntilipschitzWith K f → UniformContinuous f → IsComplete (Set.range f)

Defined in: Mathlib.Topology.MetricSpace.Antilipschitz
Cited by: 1 results in Mathlib
Foundations: Depth 150 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: PseudoEMetricSpace PseudoEMetricSpace CompleteSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Set.rangestatement · cited by 4,705
NNRealstatement and proof · cited by 4,310
CompleteSpacestatement and proof · cited by 2,532
PseudoEMetricSpacestatement and proof · cited by 1,536
UniformContinuousstatement and proof · cited by 410
AntilipschitzWithstatement and proof · cited by 132
IsCompletestatement · cited by 68
AntilipschitzWith.isUniformInducingproof · cited by 8
IsUniformInducing.isComplete_rangeproof · cited by 4

Cited by1

Results whose statement or proof uses this declaration.

AntilipschitzWith.isClosed_rangeproof · cited by 4