mem_uniformity_iff — Mathlib

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]

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