congr

Mathlib.Topology.ContinuousOn

URI: https://scilib.ai/kg/mathlib#ContinuousOn.congr

English

If g agrees with f on s, then ContinuousOn g s iff ContinuousOn f s.

Русский

Если g совпадает с f на s, то ContinuousOn g s эквивално ContinuousOn f s.

LaTeX

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

Lean4

theorem congr (h : ContinuousOn f s) (h' : EqOn g f s) : ContinuousOn g s :=
  h.congr_mono h' (Subset.refl _)

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

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

Разделы

Аффилиация

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