English
Let α be a uniform space whose uniformity 𝓤α has a basis {s_i} with p_i describing the basis. Then for x, y ∈ α, x and y are inseparable if and only if (x, y) lies in every basis member s_i for which p_i holds; equivalently, (x, y) ∈ s_i for all i with p_i.
Русский
Пусть α — равномерное пространство, у которого базис единств 𝓤α задаётся парами (i, s_i) с условием p_i. Тогда точки x, y ∈ α неразделимы тогда и только тогда, когда (x, y) принадлежит каждому элементу базиса s_i при условии p_i; то есть (x, y) ∈ s_i для всех i с p_i.
LaTeX
$$$\text{Inseparable}(x,y) \;\Longleftrightarrow\; \forall i,\ p(i) \rightarrow (x,y) \in s(i)$$$
Lean4
theorem inseparable_iff_uniformity {ι : Sort*} {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s) {x y : α} :
Inseparable x y ↔ ∀ i, p i → (x, y) ∈ s i :=
specializes_iff_inseparable.symm.trans h.specializes_iff_uniformity
