English
If a HasBasis p s for 𝓤 α holds, then t ∈ 𝓤 α iff there exists i with p i and ∀ a,b, (a,b) ∈ s i → (a,b) ∈ t.
Русский
Если имеется базис HasBasis p s для 𝓤 α, тогда t ∈ 𝓤 α тогда и только тогда, существует i с p i и для всех a,b, если (a,b) ∈ s i, то (a,b) ∈ t.
LaTeX
$$$t ∈ 𝓤 α \iff ∃ i, p i ∧ ∀ a b, (a,b) ∈ s i \rightarrow (a,b) ∈ t$$$
Lean4
theorem mem_uniformity_iff {p : β → Prop} {s : β → Set (α × α)} (h : (𝓤 α).HasBasis p s) {t : Set (α × α)} :
t ∈ 𝓤 α ↔ ∃ i, p i ∧ ∀ a b, (a, b) ∈ s i → (a, b) ∈ t :=
h.mem_iff.trans <| by simp only [Prod.forall, subset_def]