support_single_subset

Mathlib.Data.Finsupp.Single

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

← MathLib Explorer

English

The support of single a b is a subset of {a}.

Русский

Опора single a b является подмножеством множества {a}.

LaTeX

$$$$\\operatorname{supp}(\\text{single } a\\, b)\\subseteq \\{a\\}.$$$$

Lean4

theorem support_single_subset : (single a b).support ⊆ { a } := by
  classical
  simp only [single]
  split_ifs <;> [exact empty_subset _; exact Subset.refl _]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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