OAI/Analysis/BoundedHochschild/CompactConvexCenter.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A compact nontrivial set has a convex average strictly closer than its diameter.

  1. theorem OAI.BoundedHochschild.KadisonRingrose.compact_convex_center line 23

    Source documentation

    The elementary normal-structure argument needed for the isometric fixed-point theorem.

    theorem compact_convex_center (K : Set E) (hK : IsCompact K) (hnt : K.Nontrivial) :
    ∃ z ∈ convexHull ℝ K, ∃ r : ℝ, r < Metric.diam K ∧
      ∀ y ∈ K, ‖z - y‖ ≤ r := by
…