locallyLipschitzOn_iff_restrict — Mathlib

English

LocallyLipschitzOn s f is equivalent to LocallyLipschitz (s.restrict f).

Русский

LocallyLipschitzOn s f эквивалентно LocallyLipschitz (s.restrict f).

LaTeX

$$$LocallyLipschitzOn(s,f)\iff LocallyLipschitz(s.restrict f)$$$

Lean4

theorem locallyLipschitzOn_iff_restrict : LocallyLipschitzOn s f ↔ LocallyLipschitz (s.restrict f) :=
  by
  simp only [LocallyLipschitzOn, LocallyLipschitz, SetCoe.forall', lipschitzOnWith_restrict,
    nhds_subtype_eq_comap_nhdsWithin, mem_comap]
  congr! with x K
  constructor
  · rintro ⟨t, ht, hft⟩
    exact ⟨_, ⟨t, ht, Subset.rfl⟩, hft.mono <| inter_subset_right.trans <| image_preimage_subset ..⟩
  · rintro ⟨t, ⟨u, hu, hut⟩, hft⟩
    exact ⟨s ∩ u, Filter.inter_mem self_mem_nhdsWithin hu, hft.mono fun x hx ↦ ⟨hx.1, ⟨x, hx.1⟩, hut hx.2, rfl⟩⟩

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