mk_of_hasBasis — Mathlib

English

If V is transitive and V ∈ 𝓤 X, then ball x V is open.

Русский

Если V транзитивно и V ∈ 𝓤 X, то шар вокруг x по V открыт.

LaTeX

$$$\text{Transitive}(V) \land V \in \mathcal{U}(X) \Rightarrow \mathrm{ball}(x,V) \text{ is open}$$$

Lean4

theorem mk_of_hasBasis {ι : Type*} {p : ι → Prop} {s : ι → Set (X × X)} (h_basis : (𝓤 X).HasBasis p s)
    (h_symm : ∀ i, p i → IsSymmetricRel (s i)) (h_trans : ∀ i, p i → IsTransitiveRel (s i)) : IsUltraUniformity X where
  hasBasis :=
    h_basis.to_hasBasis' (fun i hi ↦ ⟨s i, ⟨h_basis.mem_of_mem hi, h_symm i hi, h_trans i hi⟩, subset_rfl⟩)
      (fun _ hs ↦ hs.1)

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