cauchy_iff_le — Mathlib

English

For l: Filter α with l.NeBot, the Cauchy condition is equivalent to l ×ˢ l ≤ 𝓤 α when interpreted as a condition on products.

Русский

Для фильтра l на α с l.NeBot условие Коши эквивалентно l ×ˢ l ≤ 𝓤 α, когда это трактуется через произведение.

LaTeX

$$$ \forall l:\text{Filter }\alpha\;[l.\text{NeBot}]\;: \text{Cauchy}(l) \iff l \timesˢ l \le 𝓤\_\alpha$$$

Lean4

theorem cauchy_iff_le {l : Filter α} [hl : l.NeBot] : Cauchy l ↔ l ×ˢ l ≤ 𝓤 α := by simp only [Cauchy, hl, true_and]

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