mem_uniformity_isClosed — Mathlib

English

For any entourage s, there exists a closed entourage t ⊆ s with t ∈ 𝓤 α.

Русский

Для любого энтурджа s существует замкнутый энтурдж t ⊆ s, при этом t ∈ 𝓤 α.

LaTeX

$$$s ∈ 𝓤 α \Rightarrow ∃ t ∈ 𝓤 α, IsClosed t ∧ t ⊆ s$$$

Lean4

theorem mem_uniformity_isClosed {s : Set (α × α)} (h : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, IsClosed t ∧ t ⊆ s :=
  let ⟨t, ⟨ht_mem, htc⟩, hts⟩ := uniformity_hasBasis_closed.mem_iff.1 h
  ⟨t, ht_mem, htc, hts⟩

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