einfsep_lt_iff — Mathlib

English

For any d, s.einfsep < d iff there exist two distinct points of s at distance less than d.

Русский

Для любого d: s.einfsep < d эквивалентно существованию двух различных точек в s на расстоянии меньше d.

LaTeX

$$$s.einfsep < d \iff \exists x \in s, \exists y \in s, x \neq y \land edist x y < d$$$

Lean4

theorem einfsep_lt_iff {d} : s.einfsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < d := by
  simp_rw [einfsep, iInf_lt_iff, exists_prop]

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