support_monotone

Mathlib.Data.Finsupp.Order

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

← MathLib Explorer

English

The support map is monotone: if f ≤ g then supp(f) ⊆ supp(g).

Русский

Отображение поддержки монотонно: если f ≤ g, то supp(f) ⊆ supp(g).

LaTeX

$$Monotone Finsupp.support$$

Lean4

theorem support_monotone : Monotone (support (α := ι) (M := α)) := fun f g h a ha ↦ by
  rw [mem_support_iff, ← pos_iff_ne_zero] at ha ⊢; exact ha.trans_le (h _)

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

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

Разделы

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

Аффилиация

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