strictMono_nhdsSet — Mathlib

English

The mapping s ↦ 𝓝ˢ(s) is strictly monotone with respect to inclusion: if s ⊊ t then 𝓝ˢ(s) ⊊ 𝓝ˢ(t).

Русский

Отображение s ↦ 𝓝ˢ(s) строго монотонно по включению: если s ⊊ t, то 𝓝ˢ(s) ⊊ 𝓝ˢ(t).

LaTeX

$$$\text{If } s \subsetneq t, \text{ then } 𝓝^{\mathrm{set}}(s) \subsetneq 𝓝^{\mathrm{set}}(t).$$$

Lean4

theorem strictMono_nhdsSet [T1Space X] : StrictMono (𝓝ˢ : Set X → Filter X) :=
  monotone_nhdsSet.strictMono_of_injective injective_nhdsSet

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