subtype_mk — Mathlib

English

If f is K-Lipschitz and every f x satisfies a predicate p, then the map x ↦ ⟨f x, hp x⟩ is K-Lipschitz into the subtype defined by p.

Русский

Если f на A удовлетворяет условию липшицивости с константой K и каждый образ f x удовлетворяет предикату p, то отображение x ↦ ⟨f x, hp x⟩ из A в субтип {y | p y} является K‑липшицевым.

LaTeX

$$$\\text{LipschitzWith } K (\\lambda x, \\langle f x, hp x \\rangle) : α \\to { y \\mid p(y) }$$$

Lean4

theorem subtype_mk (hf : LipschitzWith K f) {p : β → Prop} (hp : ∀ x, p (f x)) :
    LipschitzWith K (fun x => ⟨f x, hp x⟩ : α → { y // p y }) :=
  hf

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