continuousWithinAt_union — Mathlib

English

Continuity within a union equals conjunction of continuities: f is continuous within s ∪ t at x iff f is continuous within s at x and within t at x.

Русский

Непрерывность на объединении равна объединению непрерывностей: f непрерывна на s ∪ t в x тогда и только тогда, когда она непрерывна на s в x и на t в x.

LaTeX

$$$$\text{ContinuousWithinAt}(f, s \cup t, x) \;\iff\; \text{ContinuousWithinAt}(f, s, x) \land \text{ContinuousWithinAt}(f, t, x)$$$$

Lean4

theorem continuousWithinAt_union :
    ContinuousWithinAt f (s ∪ t) x ↔ ContinuousWithinAt f s x ∧ ContinuousWithinAt f t x := by
  simp only [ContinuousWithinAt, nhdsWithin_union, tendsto_sup]

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