comp3_mem_uniformity — Mathlib

English

If s ∈ 𝓤 α, then there exist t ∈ 𝓤 α with t ∘ (t ∘ t) ⊆ s.

Русский

Пусть s ∈ 𝓤 α; тогда существует t ∈ 𝓤 α с t ∘ (t ∘ t) ⊆ s.

LaTeX

$$$$\\forall s ∈ 𝓤 α,\\; \\exists t ∈ 𝓤 α:\\ t \\circ (t \\circ t) ⊆ s.$$$$

Lean4

theorem comp3_mem_uniformity {s : Set (α × α)} (hs : s ∈ 𝓤 α) : ∃ t ∈ 𝓤 α, t ○ (t ○ t) ⊆ s :=
  let ⟨_t', ht', ht's⟩ := comp_mem_uniformity_sets hs
  let ⟨t, ht, htt'⟩ := comp_mem_uniformity_sets ht'
  ⟨t, ht, (compRel_mono ((subset_comp_self (refl_le_uniformity ht)).trans htt') htt').trans ht's⟩

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