mono — Mathlib

English

If u1 ≤ u2 are two uniform structures on γ, then the corresponding uniformities 𝒰(α, γ, u1) ≤ 𝒰(α, γ, u2).

Русский

Если u1 ≤ u2 — две равномерности на γ, тогда получаются 𝒰(α, γ, u1) ≤ 𝒰(α, γ, u2).

LaTeX

$$$$ u_1 \le u_2 \quad\Rightarrow\quad 𝒰(α, γ, u_1) \le 𝒰(α, γ, u_2). $$$$

Lean4

/-- If `u₁` and `u₂` are two uniform structures on `γ` and `u₁ ≤ u₂`, then
`𝒰(α, γ, u₁) ≤ 𝒰(α, γ, u₂)`. -/
protected theorem mono : Monotone (@UniformFun.uniformSpace α γ) := fun _ _ hu => (UniformFun.gc α γ).monotone_u hu

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