Theorems · Theorem · general topology

IsUltrametricDist.closedBall_subset_trichotomy

∀ {X : Type u_1} [inst : PseudoMetricSpace X] [IsUltrametricDist X] (x y : X) (r s : ℝ),
  Metric.closedBall x r ⊆ Metric.closedBall y s ∨
    Metric.closedBall y s ⊆ Metric.closedBall x r ∨ Disjoint (Metric.closedBall x r) (Metric.closedBall y s)

Defined in

Mathlib.Topology.MetricSpace.Ultra.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceIsUltrametricDist