continuous_of_mulTSupport — Mathlib

English

An x is not in mulTSupport f iff f is eventually equal to 1 near x.

Русский

x не принадлежит mulTSupport f тогда и только тогда, когда f ≈ 1 в окрестности x.

LaTeX

$$$\forall x, x \notin \operatorname{mulTSupport}(f) \iff f =_{\mathcal{N}_x} 1$$$

Lean4

@[to_additive]
theorem continuous_of_mulTSupport [TopologicalSpace β] {f : α → β} (hf : ∀ x ∈ mulTSupport f, ContinuousAt f x) :
    Continuous f :=
  continuous_iff_continuousAt.2 fun x =>
    (em _).elim (hf x) fun hx =>
      (@continuousAt_const _ _ _ _ _ 1).congr (notMem_mulTSupport_iff_eventuallyEq.mp hx).symm

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