inf_eq — Mathlib

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

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