isUniformEmbedding_inr — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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