lift'_comp_uniformity — Mathlib

English

The lifted composition equals the uniformity: the composition of the uniformity with itself yields the uniformity.

Русский

Вознесённая композиция равномерности равна самой равномерности: композиция равномерности с самой собой дает равномерность.

LaTeX

$$$((𝓤 α).lift' (\\lambda s. s \\circ s)) = 𝓤 α$$$

Lean4

theorem lift'_comp_uniformity : ((𝓤 α).lift' fun s : Set (α × α) => s ○ s) = 𝓤 α :=
  comp_le_uniformity.antisymm <|
    le_lift'.2 fun _s hs ↦ mem_of_superset hs <| subset_comp_self <| idRel_subset.2 fun _ ↦ refl_mem_uniformity hs

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