supported_univ

Mathlib.LinearAlgebra.Finsupp.Supported

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

English

The supported submodule on the universal set is the top submodule.

Русский

Поддерживаемый подмодуль на всём множестве равен верхнему подмодулю.

LaTeX

$$$\mathrm{supported}(M,R,\mathrm{Set.univ}) = \top$$$

Lean4

@[simp]
theorem supported_univ : supported M R (Set.univ : Set α) = ⊤ :=
  eq_top_iff.2 fun _ _ => Set.subset_univ _

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

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

Разделы

Аффилиация

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