einfsep_lt_top — Mathlib

English

s.einfsep is finite iff there exist two points in s with finite distance between them.

Русский

s.einfsep конечно, тогда и только тогда, когда существуют две точки в s с конечным расстоянием между ними.

LaTeX

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

Lean4

theorem einfsep_lt_top : s.einfsep < ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ∞ := by
  simp_rw [einfsep, iInf_lt_iff, exists_prop]

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