support_onFinset_subset

Mathlib.Data.Finsupp.Defs

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

← MathLib Explorer

English

The support of onFinset is contained in s.

Русский

Опора onFinset вложена в s.

LaTeX

$$(onFinset s f hf).support ⊆ s$$

Lean4

@[simp]
theorem support_onFinset_subset {s : Finset α} {f : α → M} {hf} : (onFinset s f hf).support ⊆ s := by
  classical
  rw [support_onFinset]
  exact filter_subset (f · ≠ 0) s

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

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

Разделы

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

Аффилиация

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