isUniformEmbedding_set_inclusion — Mathlib

English

If s ⊆ t are subsets of α, then the inclusion map from s to t is a uniform embedding (with the subspace uniformities).

Русский

Если s ⊆ t являются подмножествами α, то отображение включения s → t является равномерным вложением (с подпространственными равномерностями).

LaTeX

$$$\\displaystyle \\text{IsUniformEmbedding}(\\iota_{st})\\;\\text{ for } s\\subseteq t$, where $\\iota_{st}$ is the inclusion map $s\\hookrightarrow t$.$$

Lean4

theorem isUniformEmbedding_set_inclusion {s t : Set α} (hst : s ⊆ t) : IsUniformEmbedding (inclusion hst)
    where
  comap_uniformity := by rw [uniformity_subtype, uniformity_subtype, comap_comap]; rfl
  injective := inclusion_injective hst

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