English
Assume u1 ≤ u2 on γ and 𝔖2 ⊆ 𝔖1. Then the convergence-structure 𝒱(α, γ, 𝔖1, u1) is below or equal to 𝒱(α, γ, 𝔖2, u2).
Русский
Пусть u1 ≤ u2 на γ и 𝔖2 ⊆ 𝔖1. Тогда структура схода 𝒱(α, γ, 𝔖1, u1) меньшая либо равна 𝒱(α, γ, 𝔖2, u2).
LaTeX
$$$(u_1 \\le u_2) \\land (\\mathfrak{S}_2 \\subseteq \\mathfrak{S}_1) \\Rightarrow \\mathcal{V}(\\alpha, \\gamma, \\mathfrak{S}_1, u_1) \\le \\mathcal{V}(\\alpha, \\gamma, \\mathfrak{S}_2, u_2).$$$
Lean4
/-- Let `u₁`, `u₂` be two uniform structures on `γ` and `𝔖₁ 𝔖₂ : Set (Set α)`. If `u₁ ≤ u₂` and
`𝔖₂ ⊆ 𝔖₁` then `𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₂)`. -/
protected theorem mono ⦃u₁ u₂ : UniformSpace γ⦄ (hu : u₁ ≤ u₂) ⦃𝔖₁ 𝔖₂ : Set (Set α)⦄ (h𝔖 : 𝔖₂ ⊆ 𝔖₁) :
𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₂) :=
calc
𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₁) := iInf_le_iInf_of_subset h𝔖
_ ≤ 𝒱(α, γ, 𝔖₂, u₂) := iInf₂_mono fun _i _hi => UniformSpace.comap_mono <| UniformFun.mono hu
