diff_iff — Mathlib

English

If f is continuous within t at x, then f is continuous within s \ t at x iff f is continuous within s at x.

Русский

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

LaTeX

$$$$\text{ContinuousWithinAt}(f, t, x) \Rightarrow \bigl(\text{ContinuousWithinAt}(f, s \setminus t, x) \iff \text{ContinuousWithinAt}(f, s, x)\bigr).$$$$

Lean4

theorem diff_iff (ht : ContinuousWithinAt f t x) : ContinuousWithinAt f (s \ t) x ↔ ContinuousWithinAt f s x :=
  ⟨fun h => (h.union ht).mono <| by simp only [diff_union_self, subset_union_left], fun h => h.mono diff_subset⟩

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