continuousWithinAt_inter' — Mathlib

English

If t belongs to the neighborhood filter of x restricted to s, then f is continuous within s ∩ t at x if and only if f is continuous within s at x.

Русский

Если t принадлежит фильтру окрестностей x, ограниченному s, то f непрерывна на s ∩ t в точке x тогда и только тогда, когда f непрерывна на s в x.

LaTeX

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

Lean4

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

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