continuousWithinAt_inter — Mathlib

English

If t is a neighborhood of x in the ambient space, then f is continuous within (s ∩ t) at x iff f is continuous within s at x.

Русский

Если t является окрестностью x в пространстве, то f непрерывна на s ∩ t в x тогда и только тогда, когда она непрерывна на s в x.

LaTeX

$$$$t \in 𝓝x \Rightarrow \text{ContinuousWithinAt}(f, s \cap t, x) \iff \text{ContinuousWithinAt}(f, s, x)$$$$

Lean4

theorem continuousWithinAt_inter (h : t ∈ 𝓝 x) : ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x := by
  simp [ContinuousWithinAt, nhdsWithin_restrict' s h]

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