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]