le_einfsep_iff — Mathlib

English

For any d, d ≤ s.einfsep iff for all x,y in s with x ≠ y we have d ≤ edist x y.

Русский

Для любого d верно: d ≤ s.einfsep тогда и только тогда, когда для всех x,y ∈ s с x ≠ y выполняется d ≤ edist x y.

LaTeX

$$$d \le s.einfsep \iff \forall x \in s, \forall y \in s, x \neq y \rightarrow d \le edist\, x\, y$$$

Lean4

theorem le_einfsep_iff {d} : d ≤ s.einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ edist x y := by
  simp_rw [einfsep, le_iInf_iff]

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