isUniformEmbedding_inl — Mathlib

English

The left injection from a space into a sum is a uniform embedding.

Русский

Левый инъектор из пространства в сумму является равномерным вложением.

LaTeX

$$$\\text{IsUniformEmbedding} (\\text{Sum.inl})$$$

Lean4

theorem isUniformEmbedding_inl : IsUniformEmbedding (Sum.inl : α → α ⊕ β) :=
  isUniformEmbedding_iff'.2
    ⟨Sum.inl_injective, uniformContinuous_inl, fun s hs =>
      ⟨Prod.map Sum.inl Sum.inl '' s ∪ range (Prod.map Sum.inr Sum.inr), union_mem_sup (image_mem_map hs) range_mem_map,
        fun x h => by simpa [Prod.map_apply'] using h⟩⟩

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