inter — Mathlib

English

If s has unique differentiability and t is open, then s ∩ t has unique differentiability.

Русский

Если у множества s есть уникальная дифференцируемость, а множество t открыто, то s ∩ t также имеет уникальную дифференциируемость.

LaTeX

$$$ \\operatorname{UniqueDiffOn}_{\\mathbb{k}}(s) \\Rightarrow \\operatorname{IsOpen}(t) \\Rightarrow \\operatorname{UniqueDiffOn}_{\\mathbb{k}}(s \\cap t) $$$

Lean4

theorem inter (hs : UniqueDiffOn 𝕜 s) (ht : IsOpen t) : UniqueDiffOn 𝕜 (s ∩ t) := fun x hx =>
  (hs x hx.1).inter (IsOpen.mem_nhds ht hx.2)

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