inter' — Mathlib

English

Variants of unique diff within at with intersection and restricted neighborhoods.

Русский

Варианты уникальной дифференцируемости внутри пересечения с ограниченными окрестностями.

LaTeX

$$$\\text{inter'}(hs, ht) : UniqueDiffWithinAt_{\\mathbb{k}}(s \\cap t, x) \\iff UniqueDiffWithinAt_{\\mathbb{k}}(s, x)$$$

Lean4

theorem inter' (hs : UniqueDiffWithinAt 𝕜 s x) (ht : t ∈ 𝓝[s] x) : UniqueDiffWithinAt 𝕜 (s ∩ t) x :=
  (uniqueDiffWithinAt_inter' ht).2 hs

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