uniformContinuous_subtype_val — Mathlib

English

The inclusion from a subtype to the ambient space is uniformly continuous.

Русский

Включение подмножества в общую область равномерно непрерывно.

LaTeX

$$$$\\mathrm{UniformContinuous}(\\mathrm{Subtype}.val : {a:\\alpha // p a} \\\\to \\alpha).$$$$

Lean4

theorem uniformContinuous_subtype_val {p : α → Prop} [UniformSpace α] :
    UniformContinuous (Subtype.val : { a : α // p a } → α) :=
  uniformContinuous_comap

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