inter' — Mathlib

English

For a Besicovitch SatelliteConfig a and i, the distance dist(a.c(i), a.c(last N)) is bounded by a.r(i) + a.r(last N).

Русский

Для конфигурации спутников Бесиковича расстояние между центрами удерживаемых спутников ограничено суммой соответствующих радиусов.

LaTeX

$$∀ i, dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)$$

Lean4

theorem inter' (i : Fin N.succ) : dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N) :=
  by
  rcases lt_or_ge i (last N) with (H | H)
  · exact a.inter i H
  · have I : i = last N := top_le_iff.1 H
    have := (a.rpos (last N)).le
    simp only [I, add_nonneg this this, dist_self]

Похожие утверждения