Theorems · Theorem · general topology

nndist_pi_lt_iff

∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)]
  {f g : (b : β) → X b} {r : NNReal}, 0 < r → (nndist f g < r ↔ ∀ (b : β), nndist (f b) (g b) < r)

Defined in

Mathlib.Topology.MetricSpace.Pseudo.Pi

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypePseudoMetricSpace