einfsep_top — Mathlib

English

The extended infimum separation equals infinity exactly when every pair of distinct points in s is at infinite distance.

Русский

Расширенная инфиминальная разделённость равна бесконечности тогда и только тогда, когда расстояние между любыми двумя различными точками множества s является бесконечным.

LaTeX

$$$s.einfsep = \infty \iff \forall x \in s, \forall y \in s, x \neq y \rightarrow edist\, x\, y = \infty$$$

Lean4

theorem einfsep_top : s.einfsep = ∞ ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ∞ := by simp_rw [einfsep, iInf_eq_top]

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