English
The indexed infimum (iInf) of a family of uniform spaces carries an ultra-uniformity provided each component space is ultra-uniform.
Русский
Индексированное пересечение семейства пространств имеет ультра-равномерность, если каждая точка семейства обладает ею.
LaTeX
$$$@IsUltraUniformity\ _ {X} (\big( \bigwedge i U_i \big) )$$$
Lean4
theorem iInf {ι : Type*} {U : (i : ι) → UniformSpace X} (hU : ∀ i, @IsUltraUniformity X (U i)) :
@IsUltraUniformity _ (⨅ i, U i : UniformSpace X) :=
by
letI : UniformSpace X := ⨅ i, U i
refine .mk_of_hasBasis (iInf_uniformity ▸ Filter.HasBasis.iInf fun i ↦ (hU i).hasBasis) ?_ ?_
· exact fun _ ⟨_, h⟩ ↦ IsSymmetricRel.iInter fun i ↦ (h i).right.left
· exact fun _ ⟨_, h⟩ ↦ IsTransitiveRel.iInter fun i ↦ (h i).right.right
