mem_filterAt_iff — Mathlib

English

For h, the coverings indexed by the subtype h.index are pairwise disjoint.

Русский

Для h покрытия, индексируемые подтипом h.index, попарно несовпадающие.

LaTeX

$$$Pairwise\\ (Disjoint\\ on\\ (fun x:\\, h.index\\Rightarrow h.covering x)).$$$

Lean4

theorem mem_filterAt_iff {x : X} {s : Set (Set X)} :
    s ∈ v.filterAt x ↔ ∃ ε > (0 : ℝ), ∀ t ∈ v.setsAt x, t ⊆ closedBall x ε → t ∈ s := by
  simp only [(v.filterAt_basis_closedBall x).mem_iff, ← and_imp, subset_def, mem_setOf]

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