Theorems · Theorem · general topology

Set.Finite.infsep

∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α} [inst_1 : Decidable s.Nontrivial] (hsf : s.Finite),
  s.infsep = if hs : s.Nontrivial then ⋯.toFinset.inf' ⋯ (Function.uncurry dist) else 0

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites15

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
Realstatement and proof · cited by 25,697
Set.Finitestatement and proof · cited by 1,814
PseudoMetricSpacestatement and proof · cited by 1,550
Dist.diststatement and proof · cited by 1,539
Set.Finite.toFinsetstatement and proof · cited by 351
Set.Nontrivialstatement and proof · cited by 145
Finset.inf'statement and proof · cited by 117
eq_of_forall_le_iffproof · cited by 65
Set.infsepstatement and proof · cited by 35
Set.offDiagstatement · cited by 35
Set.not_nontrivial_iffproof · cited by 13

Cited by1

Results whose statement or proof uses this declaration.

Set.Finite.infsep_of_nontrivialproof · cited by 0