continuousOn_congr

Mathlib.Topology.ContinuousOn

URI: https://scilib.ai/kg/mathlib#continuousOn_congr

English

If f and g are equal on s, then ContinuousOn f s ↔ ContinuousOn g s.

Русский

Если f и g равны на s, то ContinuousOn f s эквивално ContinuousOn g s.

LaTeX

$$$$\text{EqOn}(g,f,s) \Rightarrow (\text{ContinuousOn}(g,s) \iff \text{ContinuousOn}(f,s)).$$$$

Lean4

theorem continuousOn_congr (h' : EqOn g f s) : ContinuousOn g s ↔ ContinuousOn f s :=
  ⟨fun h => ContinuousOn.congr h h'.symm, fun h => h.congr h'⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru