einfsep_zero — Mathlib

English

The value s.einfsep is zero precisely when for every positive C there exist two distinct points in s whose distance is less than C.

Русский

Значение s.einfsep равно нулю тогда и только тогда, когда для любого положительного C существуют две различные точки x,y в s с edist x y < C.

LaTeX

$$$s.einfsep = 0 \iff \forall C>0, \exists x \in s, \exists y \in s, x \neq y \land edist\, x\, y < C$$$

Lean4

theorem einfsep_zero : s.einfsep = 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C := by
  simp_rw [einfsep, ← _root_.bot_eq_zero, iInf_eq_bot, iInf_lt_iff, exists_prop]

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