isSupported_upwards

Mathlib.RingTheory.FreeCommRing

URI: https://scilib.ai/kg/mathlib#FreeCommRing.isSupported_upwards

English

If x is supported on s and s ⊆ t, then x is supported on t.

Русский

Если x поддержано на s и s ⊆ t, то x поддержано на t.

LaTeX

$$$ (\\text{IsSupported}\\, x\\, s) \\land (s \\subseteq t) \\Rightarrow \\text{IsSupported}(x, t) $$$

Lean4

theorem isSupported_upwards (hs : IsSupported x s) (hst : s ⊆ t) : IsSupported x t :=
  Subring.closure_mono (Set.monotone_image hst) hs

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

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

Разделы

Аффилиация

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