comp_le_uniformity3 — Mathlib

English

For monotone f, ((𝓤 α).lift' (λ s, s ○ (s ○ s))) ≤ 𝓤 α.

Русский

Для монотонной f справедливо ((𝓤 α).lift' (λ s, s ∘ (s ∘ s))) ≤ 𝓤 α.

LaTeX

$$$$\\forall {f} (hg : Monotone f), ((𝓤 α).lift' (\\lambda s : Set(α × α), s \\circ (s \\circ s))) \\le (𝓤 α).$$$$

Lean4

/-- See also `comp3_mem_uniformity`. -/
theorem comp_le_uniformity3 : ((𝓤 α).lift' fun s : Set (α × α) => s ○ (s ○ s)) ≤ 𝓤 α := fun _ h =>
  let ⟨_t, htU, ht⟩ := comp3_mem_uniformity h
  mem_of_superset (mem_lift' htU) ht

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