touchpoint_empty_injective — Mathlib

English

If excenters exist for a set of signs, the touchpoint map is injective.

Русский

Отображение индексов в точки касания инъективно при наличии соответствующего эксцентрирования.

LaTeX

$$For all signs, h.ExcenterExists signs → Function.Injective (s.touchpoint signs)$$

Lean4

theorem touchpoint_empty_injective : Function.Injective (s.touchpoint ∅) :=
  s.excenterExists_empty.touchpoint_injective

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