uniformSpace_eq_bot — Mathlib

English

If the uniformity has a basis (p, s), then u = ⊥ iff there exists i with p(i) and every pair x ≠ y is not related by s(i).

Русский

Если у равномерности есть базис (p, s), то u = ⊥ тогда и только тогда, когда существует i с p(i) и для всех x ≠ y пары (x,y) не принадлежат s(i).

LaTeX

$$u = ⊥ ⇔ ∃ i, p i ∧ Pairwise (λ x y, (x,y) ∉ s i)$$

Lean4

protected theorem _root_.Filter.HasBasis.uniformSpace_eq_bot {ι p} {s : ι → Set (α × α)} {u : UniformSpace α}
    (h : 𝓤[u].HasBasis p s) : u = ⊥ ↔ ∃ i, p i ∧ Pairwise fun x y : α ↦ (x, y) ∉ s i := by
  simp [uniformSpace_eq_bot, h.mem_iff, subset_def, Pairwise, not_imp_not]

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