subtype_mk — Mathlib

English

If f: β → α is uniformly continuous and ∀ x, p(f x), then x ↦ ⟨f x, h x⟩ is uniformly continuous from β to Subtype p.

Русский

Если f: β → α равномерно непрерывна и ∀ x, p(f x), то отображение x ↦ ⟨f x, h x⟩ из β в Subtype p равно равномерно непрерывному.

LaTeX

$$$$\\text{hf: UniformContinuous } f\\;\\land\\; \\forall x, p(f x) \\Rightarrow \\text{UniformContinuous}(\\lambda x, \\langle f x, h x \\rangle).$$$$

Lean4

theorem subtype_mk {p : α → Prop} [UniformSpace α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f)
    (h : ∀ x, p (f x)) : UniformContinuous (fun x => ⟨f x, h x⟩ : β → Subtype p) :=
  uniformContinuous_comap' hf

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