infsep_pos — Mathlib

English

The positivity of infsep is equivalent to finiteness of Einfsep: 0 < s.infsep iff 0 < s.einfsep and s.einfsep < ∞.

Русский

Положительность s.infsep эквивалентна конечности s.einfsep: 0 < s.infsep ⇔ 0 < s.einfsep ∧ s.einfsep < ∞.

LaTeX

$$$ 0 < s.infsep \leftrightarrow (0 < s.einfsep \land s.einfsep < \infty) $$$

Lean4

theorem infsep_pos : 0 < s.infsep ↔ 0 < s.einfsep ∧ s.einfsep < ∞ := by simp_rw [infsep, ENNReal.toReal_pos_iff]

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