infsep_zero — Mathlib

English

For any set s in an edist space, s.infsep = 0 precisely when s.einfsep = 0 or s.einfsep = ∞.

Русский

Для множества s в пространстве с затратой расстояния: s.infsep = 0 тогда, и только тогда, когда s.einfsep = 0 или s.einfsep = ∞.

LaTeX

$$$ s.infsep = 0 \leftrightarrow (s.einfsep = 0 \lor s.einfsep = \infty) $$$

Lean4

theorem infsep_zero : s.infsep = 0 ↔ s.einfsep = 0 ∨ s.einfsep = ∞ := by rw [infsep, ENNReal.toReal_eq_zero_iff]

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