CAT(0) spaces

DefinitionCAT(0) four-point condition#✓fully proved

A metric space \(X\) satisfies the CAT(0) four-point comparison condition if for all points \(x, y, z, w \in X\) (not necessarily distinct),

\[d(x, z)^2 + d(y, w)^2 \le d(x, y)^2 + d(y, z)^2 + d(z, w)^2 + d(w, x)^2,\]

that is, the sum of the squares of the diagonals of every quadrilateral \(xyzw\) is at most the sum of the squares of its sides.

For geodesic metric spaces this is equivalent to the usual Euclidean comparison-triangle definition of a CAT(0) space.

def IsCAT0FourPoint (X : Type u) [MetricSpace X] : Prop :=
  ∀ x y z w : X,
    dist x z ^ 2 + dist y w ^ 2 ≤
      dist x y ^ 2 + dist y z ^ 2 + dist z w ^ 2 + dist w x ^ 2

Used by 4

Used byIsometry invariance of the CAT(0) four-point condition · Unfolding the CAT(0) four-point condition · The CAT(0) four-point condition passes to isometrically embedded spaces · Spaces with at most one point satisfy the CAT(0) four-point condition

TheoremUnfolding the CAT(0) four-point condition#✓fully proved

A metric space \(X\) satisfies the CAT(0) four-point condition if and only if for all points \(x, y, z, w \in X\),

\[d(x, z)^2 + d(y, w)^2 \le d(x, y)^2 + d(y, z)^2 + d(z, w)^2 + d(w, x)^2.\]

theorem isCAT0FourPoint_iff {X : Type u} [MetricSpace X] :
    IsCAT0FourPoint X ↔
      ∀ x y z w : X,
        dist x z ^ 2 + dist y w ^ 2 ≤
          dist x y ^ 2 + dist y z ^ 2 + dist z w ^ 2 + dist w x ^ 2

Uses 1

Statement usesCAT(0) four-point condition

TheoremThe CAT(0) four-point condition passes to isometrically embedded spaces#✓fully proved

Let \(X\) and \(Y\) be metric spaces and let \(f : X \to Y\) be an isometry, that is, \(d(f(a), f(b)) = d(a, b)\) for all \(a, b \in X\). If \(Y\) satisfies the CAT(0) four-point condition, then so does \(X\).

theorem of_isometry {X : Type u} {Y : Type v} [MetricSpace X] [MetricSpace Y]
    (hY : IsCAT0FourPoint Y) {f : X → Y} (hf : Isometry f) : IsCAT0FourPoint X

Uses 1 · Used by 1

Statement usesCAT(0) four-point condition

Used byIsometry invariance of the CAT(0) four-point condition

TheoremIsometry invariance of the CAT(0) four-point condition#✓fully proved

If \(X\) and \(Y\) are metric spaces and there is an isometric bijection from \(X\) onto \(Y\), then \(X\) satisfies the CAT(0) four-point condition if and only if \(Y\) does.

theorem iff_of_isometryEquiv {X : Type u} {Y : Type v} [MetricSpace X] [MetricSpace Y]
    (e : X ≃ᵢ Y) : IsCAT0FourPoint X ↔ IsCAT0FourPoint Y

Uses 2

Statement usesCAT(0) four-point condition

Proof usesThe CAT(0) four-point condition passes to isometrically embedded spaces

TheoremSpaces with at most one point satisfy the CAT(0) four-point condition#✓fully proved

Every metric space with at most one point (including the empty space) satisfies the CAT(0) four-point condition.

theorem of_subsingleton (X : Type u) [MetricSpace X] [Subsingleton X] : IsCAT0FourPoint X

Uses 1

Statement usesCAT(0) four-point condition

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.