Mathlib Map

Theorems · Theorem · general topology

Set.einfsep_top

∀ {α : Type u_1} [inst : EDist α] {s : Set α}, s.einfsep = ⊤ ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ⊤
Defined in
Mathlib.Topology.MetricSpace.Infsep
Cited by
2 results in Mathlib
Foundations
Depth 127 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
EDist
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.Subsingleton.einfsep · cited by 5Subsingleton.einfsepSet.subsingleton_of_einfsep_eq_top · cited by 2Set.subsingleton_of_einfs…Set · cited by 53352SetENNReal · cited by 9879ENNRealTop.top · cited by 9680Top.topEDist.edist · cited by 735EDist.edistEDist · cited by 91EDistSet.einfsep · cited by 47Set.einfsepSet.einfsep_topCITED BYCITES

Cites6

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

  • Setstatement and proof · cited by 53,352
  • ENNRealstatement · cited by 9,879
  • Top.topstatement and proof · cited by 9,680
  • EDist.ediststatement and proof · cited by 735
  • EDiststatement and proof · cited by 91
  • Set.einfsepstatement · cited by 47

Cited by2

Results whose statement or proof uses this declaration.