inter' — Mathlib

English

If hs holds at x and t belongs to nhdsWithin x s, then UniqueMDiffWithinAt I t x holds.

Русский

Если для x выполняется hs и t ∈ nhdsWithin x s, то выполняется UniqueMDiffWithinAt I t x.

LaTeX

$$UniqueMDiffWithinAt I s x → t ∈ 𝓝[s] x → UniqueMDiffWithinAt I t x$$

Lean4

theorem inter' (hs : UniqueMDiffWithinAt I s x) (ht : t ∈ 𝓝[s] x) : UniqueMDiffWithinAt I (s ∩ t) x :=
  hs.mono_of_mem_nhdsWithin (Filter.inter_mem self_mem_nhdsWithin ht)

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