supported_mono

Mathlib.LinearAlgebra.Finsupp.Supported

URI: https://scilib.ai/kg/mathlib#Finsupp.supported_mono

English

If s ⊆ t, then the supported submodule on s is contained in the supported submodule on t.

Русский

Если s ⊆ t, то поддерживаемый подмодуль на s вложен в подмодуль на t.

LaTeX

$$$\text{If } s \subseteq t:\quad \mathrm{supported}(M,R,s) \le \mathrm{supported}(M,R,t)$$$

Lean4

theorem supported_mono {s t : Set α} (st : s ⊆ t) : supported M R s ≤ supported M R t := fun _ h =>
  Set.Subset.trans h st

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

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

Разделы

Аффилиация

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