continuousWithinAt_congr — Mathlib

English

Let f,g: X→Y and s⊆X with x∈s. If f and g coincide on s and x is in s, then ContinuousWithinAt f s x holds iff ContinuousWithinAt g s x holds.

Русский

Пусть f,g: X→Y и s⊆X с x∈s. Если f и g совпадают на s и x ∈ s, тогда непрерывность f на s в x эквивалентна непрерывности g на s в x.

LaTeX

$$$ (\forall y\in s, g(y)=f(y)) \land x\in s \Rightarrow (ContinuousWithinAt f s x \iff ContinuousWithinAt g s x).$$$

Lean4

theorem continuousWithinAt_congr (h₁ : ∀ y ∈ s, g y = f y) (hx : g x = f x) :
    ContinuousWithinAt g s x ↔ ContinuousWithinAt f s x :=
  ⟨fun h' ↦ h'.congr (fun x hx ↦ (h₁ x hx).symm) hx.symm, fun h' ↦ h'.congr h₁ hx⟩

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