subtype_map — Mathlib

English

If f: α → β is uniformly continuous and p x → q(f x), then the induced map from Subtype p to Subtype q by f is uniformly continuous.

Русский

Если f: α → β равномерно непрерывна и p x → q(f x), то отображение Subtype.map f h между подтипами равномерно непрерывно.

LaTeX

$$$$\\mathrm{UniformContinuous}(\\mathrm{Subtype.map} f h) = (hf.comp \\; \\mathrm{uniformContinuous_subtype_val}).{\\n}$$$$

Lean4

theorem subtype_map [UniformSpace α] [UniformSpace β] {p : α → Prop} {q : β → Prop} {f : α → β}
    (hf : UniformContinuous f) (h : ∀ x, p x → q (f x)) : UniformContinuous (Subtype.map f h) :=
  (hf.comp uniformContinuous_subtype_val).subtype_mk _

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