inf_eq — Mathlib

English

The uniformity obeys the infimum law: 𝒰(α, γ, u1 ⊓ u2) = 𝒰(α, γ, u1) ⊓ 𝒰(α, γ, u2).

Русский

Равномерность удовлетворяет закону Inf: 𝒰(α, γ, u1 ⊓ u2) = 𝒰(α, γ, u1) ⊓ 𝒰(α, γ, u2).

LaTeX

$$$$ 𝒰(α, γ, u_1 \sqcap u_2) = 𝒰(α, γ, u_1) \sqcap 𝒰(α, γ, 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
  -- This follows directly from the fact that the upper adjoint in a Galois connection maps
    -- infimas to infimas.

  rw [inf_eq_iInf, inf_eq_iInf, UniformFun.iInf_eq]
  refine iInf_congr fun i => ?_
  cases i <;> rfl

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