continuous_of_mulTSupport_subset — Mathlib

English

If a function is continuous at every point of its topological multiplicative support, then the function is continuous everywhere.

Русский

Если функция непрерывна во всех точках своей топологической мультипликативной опоры, то она непрерывна повсюду.

LaTeX

$$$\forall x, x \in \operatorname{mulTSupport}(f) \Rightarrow \text{ContinuousAt}(f,x) \Rightarrow \text{Continuous}(f)$$$

Lean4

@[to_additive]
theorem continuous_of_mulTSupport_subset [TopologicalSpace β] {f : α → β} {s : Set α} (hs : ContinuousOn f s)
    (h's : IsOpen s) (h''s : mulTSupport f ⊆ s) : Continuous f :=
  continuous_of_mulTSupport fun _ hx ↦ h's.continuousOn_iff.mp hs <| h''s hx

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