infsep_lt_iff — Mathlib

English

If s is Nontrivial, then s.infsep < d iff there exist x,y in s with x≠y and dist x y < d.

Русский

Если s не тривиально, то s.infsep < d эквивалентно существованию x,y∈s с x≠y и dist x y < d.

LaTeX

$$$ s.Nontrivial \rightarrow s.infsep < d \leftrightarrow \exists x \in s,\ \exists y \in s,\ x \neq y \land dist x y < d $$$

Lean4

theorem infsep_lt_iff {d} (hs : s.Nontrivial) : s.infsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ dist x y < d :=
  by
  rw [← not_iff_not]
  push_neg
  exact hs.le_infsep_iff

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