English
For two uniform structures u1 and u2 on γ, 𝒱(α, γ, 𝔖, u1 ⊓ u2) equals 𝒱(α, γ, 𝔖, u1) ⊓ 𝒱(α, γ, 𝔖, u2).
Русский
Для двух структур u1 и u2 на γ имеем 𝒱(α, γ, 𝔖, u1 ⊓ u2) = 𝒱(α, γ, 𝔖, u1) ⊓ 𝒱(α, γ, 𝔖, u2).
LaTeX
$$𝒱(α, γ, 𝔖, u_1 ⊓ u_2) = 𝒱(α, γ, 𝔖, u_1) ⊓ 𝒱(α, γ, 𝔖, u_2).$$
Lean4
/-- If `u₁` and `u₂` are two uniform structures on `γ`, then
`𝒱(α, γ, 𝔖, u₁ ⊓ u₂) = 𝒱(α, γ, 𝔖, u₁) ⊓ 𝒱(α, γ, 𝔖, u₂)`. -/
protected theorem inf_eq {u₁ u₂ : UniformSpace γ} : 𝒱(α, γ, 𝔖, u₁ ⊓ u₂) = 𝒱(α, γ, 𝔖, u₁) ⊓ 𝒱(α, γ, 𝔖, u₂) :=
by
rw [inf_eq_iInf, inf_eq_iInf, UniformOnFun.iInf_eq]
refine iInf_congr fun i => ?_
cases i <;> rfl