English
The infimum of two ultra uniformities on a set X is again an ultra uniformity: if u and u' are ultra uniformities on X, then u ⊓ u' is an ultra uniformity.
Русский
Нижняя граница двух ультра-равномерностей на пространстве X снова является ультра-равномерностью: если u и u' — ультра-равномерности на X, то u ⊓ u' — ультра-равномерность.
LaTeX
$$IsUltraUniformity u → IsUltraUniformity u' → IsUltraUniformity (u ⊓ u')$$
Lean4
theorem inf {u u' : UniformSpace X} (h : @IsUltraUniformity _ u) (h' : @IsUltraUniformity _ u') :
@IsUltraUniformity _ (u ⊓ u') := by
letI := u ⊓ u'
refine .mk_of_hasBasis (h.hasBasis.inf h'.hasBasis) ?_ ?_
· exact fun _ ⟨⟨_, hU, _⟩, _, hU', _⟩ ↦ hU.inter hU'
· exact fun _ ⟨⟨_, _, hU⟩, _, _, hU'⟩ ↦ hU.inter hU'
