iInf_eq — Mathlib

English

The uniformity 𝒱(α, γ, 𝔖, ⨅ i, u_i) equals the infimum over i of 𝒱(α, γ, 𝔖, u_i).

Русский

Структура единичного схода по совокупности 𝔖 внутри γ равна наибольшему общему снизу по i снизу 𝒱(α, γ, 𝔖, u_i).

LaTeX

$$𝒱(α, γ, 𝔖, ⨅ i, u_i) = ⨅ i, 𝒱(α, γ, 𝔖, u_i).$$

Lean4

/-- If `u` is a family of uniform structures on `γ`, then
`𝒱(α, γ, 𝔖, (⨅ i, u i)) = ⨅ i, 𝒱(α, γ, 𝔖, u i)`. -/
protected theorem iInf_eq {u : ι → UniformSpace γ} : 𝒱(α, γ, 𝔖, ⨅ i, u i) = ⨅ i, 𝒱(α, γ, 𝔖, u i) :=
  by
  simp_rw [UniformOnFun.uniformSpace, UniformFun.iInf_eq, UniformSpace.comap_iInf]
  rw [iInf_comm]
  exact iInf_congr fun s => iInf_comm

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