lipschitzOnWith_restrict — Mathlib

English

For any t ⊆ s, LipschitzOnWith K (s.restrict f) t is equivalent to LipschitzOnWith K f on their intersection with s.

Русский

Для любого t ⊆ s, LipschitzOnWith K (s.restrict f) t эквивалентно LipschitzOnWith K f на s ∩ (Subtype.val)'' t.

LaTeX

$$$LipschitzOnWith(K,(s.restrict f),t)\iff LipschitzOnWith(K,f,(s\cap (Subtype.val)'' t))$$$

Lean4

theorem lipschitzOnWith_restrict {t : Set s} :
    LipschitzOnWith K (s.restrict f) t ↔ LipschitzOnWith K f (s ∩ Subtype.val '' t) := by simp [LipschitzOnWith]

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