OAI/Analysis/SphereIsometry/DiameterBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Pairwise diameter bounds

The predicate records the distance between every pair of points. It does not use the real-valued diameter of a possibly unbounded set.

  1. def OAI.Tingley.DiameterLE line 16

    Source documentation

    Every pair of points in a set is at distance at most the given radius.

    def DiameterLE (A : Set E) (δ : ℝ) : Prop :=
…
  2. theorem OAI.Tingley.DiameterLE.mono_set line 23
  3. theorem OAI.Tingley.DiameterLE.mono_radius line 26
  4. theorem OAI.Tingley.DiameterLE.closure line 29